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