changeset 43329 | 84472e198515 |
parent 43322 | 1f6f6454f115 |
child 46219 | 426ed18eba43 |
--- a/src/Pure/Proof/proof_rewrite_rules.ML Wed Jun 08 22:16:21 2011 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 09 20:22:22 2011 +0200 @@ -200,7 +200,7 @@ fun rew_term Ts t = let val frees = - map Free (Name.invents (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts); + map Free (Name.invent (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;