more tight name invention -- avoiding old functions;

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Jun 09 11:26:25 2011 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Jun 09 15:37:37 2011 +0200
@@ -200,7 +200,7 @@
     fun rew_term Ts t =
       let
         val frees =
-          map Free (Name.invent_list (OldTerm.add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
+          map Free (Name.invents (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
         val t' = r (subst_bounds (frees, t));
         fun strip [] t = t
           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;