Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-01 18:37:23 -0800 (Wed, 01 Mar 2006)
Revision: 8811
Log message:

      When matching old subproofs with new subgoals during proof expansion, try
      keeping the old variable names in the goal intact. To do that, if the old
      subgoal (w/o the assumptions) is alpha equal to the new one, replace the goal
      (w/o the assumptions) with the old one in the new tactic arg.