changeset 18185 | 9d51fad6bb1f |
parent 18024 | 853e8219732a |
child 18708 | 4b3dadb4fe33 |
--- a/src/Pure/Proof/proof_rewrite_rules.ML Wed Nov 16 17:45:30 2005 +0100 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Wed Nov 16 17:45:31 2005 +0100 @@ -225,7 +225,7 @@ val vs = vars_of prop; val tvars = term_tvars prop; val (_, rhs) = Logic.dest_equals prop; - val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts) + val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts) (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs), map valOf ts); in