REABBREV_TAC renames duplicate abbreviations

[ordinarymath]

Given a goal of

    0.  Abbrev (a = FOO BAR)
    1.  Abbrev (a = GOO BAR)
   ------------------------------------
        test

REABBREV_TAC results in this

    0.  Abbrev (a = GOO BAR)
    1.  Abbrev (a' = FOO BAR)
   ------------------------------------
        test

[ordinarymath]

Note that this was discovered using LET_ELIM_TAC. I've also encounter other weird issues due to its rewrite based implementation that perhaps there should be a non rewrite based LET_ELIM_TAC

[mn200]

It's not clear to me that this is a problematic behaviour.

[ordinarymath]

Before REABBREV_TAC i can prove GOO BAR = FOO BAR after that i can't. I'm currently using the abbreviation to prevent var_eq_tac from exploding the goal