changeset 20076 | def4ad161528 |
parent 19482 | 9f11af8f7ef9 |
child 20664 | ffbc5a57191a |
--- 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;