src/Pure/Proof/proof_rewrite_rules.ML

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Jul 11 12:17:01 2006 +0200
@@ -194,8 +194,7 @@
   let
     fun rew_term Ts t =
       let
-        val frees = map Free (variantlist
-          (replicate (length Ts) "x", add_term_names (t, [])) ~~ Ts);
+        val frees = map Free (Name.invent_list (add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
         val t' = r (subst_bounds (frees, t));
         fun strip [] t = t
           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;