# HG changeset patch
# User wenzelm
# Date 1132159531 -3600
# Node ID 9d51fad6bb1fdd7a843d63a39298465d53016989
# Parent  43c4589a9a7856d4b502613c639f0b8684868aef
Term.betapplys;

diff -r 43c4589a9a78 -r 9d51fad6bb1f src/Pure/Isar/obtain.ML
--- 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
diff -r 43c4589a9a78 -r 9d51fad6bb1f src/Pure/Proof/proof_rewrite_rules.ML
--- 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
diff -r 43c4589a9a78 -r 9d51fad6bb1f src/ZF/Tools/datatype_package.ML
--- 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;