--- a/src/Pure/Isar/obtain.ML Wed Nov 16 17:45:30 2005 +0100
+++ b/src/Pure/Isar/obtain.ML Wed Nov 16 17:45:31 2005 +0100
@@ -225,7 +225,7 @@
val ps = map dest_Free ts;
val asms =
Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
- |> map (fn asm => (Library.foldl Term.betapply (Term.list_abs (ps, asm), ts), ([], [])));
+ |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
val _ = conditional (null asms) (fn () =>
raise Proof.STATE ("Trivial result -- nothing guessed", state));
in
--- 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
--- a/src/ZF/Tools/datatype_package.ML Wed Nov 16 17:45:30 2005 +0100
+++ b/src/ZF/Tools/datatype_package.ML Wed Nov 16 17:45:31 2005 +0100
@@ -308,7 +308,7 @@
(recursor_tm $
(list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
args)),
- subst_rec (Library.foldl betapply (recursor_case, args))));
+ subst_rec (Term.betapplys (recursor_case, args))));
val recursor_trans = recursor_def RS def_Vrecursor RS trans;