Term.betapplys;
authorwenzelm
Wed Nov 16 17:45:31 2005 +0100 (2005-11-16)
changeset 181859d51fad6bb1f
parent 18184 43c4589a9a78
child 18186 ad969501b7d4
Term.betapplys;
src/Pure/Isar/obtain.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/ZF/Tools/datatype_package.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Nov 16 17:45:30 2005 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Nov 16 17:45:31 2005 +0100
     1.3 @@ -225,7 +225,7 @@
     1.4          val ps = map dest_Free ts;
     1.5          val asms =
     1.6            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
     1.7 -          |> map (fn asm => (Library.foldl Term.betapply (Term.list_abs (ps, asm), ts), ([], [])));
     1.8 +          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
     1.9          val _ = conditional (null asms) (fn () =>
    1.10            raise Proof.STATE ("Trivial result -- nothing guessed", state));
    1.11        in
     2.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Nov 16 17:45:30 2005 +0100
     2.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Nov 16 17:45:31 2005 +0100
     2.3 @@ -225,7 +225,7 @@
     2.4                val vs = vars_of prop;
     2.5                val tvars = term_tvars prop;
     2.6                val (_, rhs) = Logic.dest_equals prop;
     2.7 -              val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts)
     2.8 +              val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
     2.9                  (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
    2.10                  map valOf ts);
    2.11              in
     3.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Nov 16 17:45:30 2005 +0100
     3.2 +++ b/src/ZF/Tools/datatype_package.ML	Wed Nov 16 17:45:31 2005 +0100
     3.3 @@ -308,7 +308,7 @@
     3.4              (recursor_tm $
     3.5               (list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
     3.6                           args)),
     3.7 -             subst_rec (Library.foldl betapply (recursor_case, args))));
     3.8 +             subst_rec (Term.betapplys (recursor_case, args))));
     3.9  
    3.10          val recursor_trans = recursor_def RS def_Vrecursor RS trans;
    3.11