# HG changeset patch # User wenzelm # Date 1307626657 -7200 # Node ID 1f6f6454f115da9a637c985bbafbdf29ce591205 # Parent 0e79cd0b315f028707c49b04266bba52a9b3e775 more tight name invention -- avoiding old functions; diff -r 0e79cd0b315f -r 1f6f6454f115 src/Pure/Proof/proof_rewrite_rules.ML --- 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;