use long names for old-style fold combinators;
authorwenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190479806475f3c
parent 30189 3633f560f4c3
child 30194 2fc281289b22
use long names for old-style fold combinators;
src/FOLP/simp.ML
src/HOL/Import/lazy_seq.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/scnp_solve.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/old_primrec_package.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/simpdata.ML
src/HOL/Tools/specification_package.ML
src/HOLCF/Tools/domain/domain_axioms.ML
src/HOLCF/Tools/domain/domain_library.ML
src/HOLCF/Tools/domain/domain_syntax.ML
src/Provers/blast.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/order.ML
src/Provers/trancl.ML
src/Provers/typedsimp.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Tools/find_consts.ML
src/Pure/library.ML
src/Pure/pure_thy.ML
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/FOLP/simp.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/FOLP/simp.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -433,7 +433,7 @@
     1.4          val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
     1.5          val new_rws = List.concat(map mk_rew_rules thms);
     1.6          val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
     1.7 -        val anet' = foldr lhs_insert_thm anet rwrls
     1.8 +        val anet' = List.foldr lhs_insert_thm anet rwrls
     1.9      in  if !tracing andalso not(null new_rws)
    1.10          then (writeln"Adding rewrites:";  Display.prths new_rws;  ())
    1.11          else ();
     2.1 --- a/src/HOL/Import/lazy_seq.ML	Sun Mar 01 16:48:06 2009 +0100
     2.2 +++ b/src/HOL/Import/lazy_seq.ML	Sun Mar 01 23:36:12 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Import/lazy_seq.ML
     2.5 -    ID:         $Id$
     2.6      Author:     Sebastian Skalberg, TU Muenchen
     2.7  
     2.8  Alternative version of lazy sequences.
     2.9 @@ -408,8 +407,8 @@
    2.10  	make (fn () => copy (f x))
    2.11      end
    2.12  
    2.13 -fun EVERY fs = foldr (op THEN) succeed fs
    2.14 -fun FIRST fs = foldr (op ORELSE) fail fs
    2.15 +fun EVERY fs = List.foldr (op THEN) succeed fs
    2.16 +fun FIRST fs = List.foldr (op ORELSE) fail fs
    2.17  
    2.18  fun TRY f x =
    2.19      make (fn () =>
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Sun Mar 01 16:48:06 2009 +0100
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Mar 01 23:36:12 2009 +0100
     3.3 @@ -777,7 +777,7 @@
     3.4                  val (c,asl) = case terms of
     3.5                                    [] => raise ERR "x2p" "Bad oracle description"
     3.6                                  | (hd::tl) => (hd,tl)
     3.7 -                val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
     3.8 +                val tg = List.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
     3.9              in
    3.10                  mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
    3.11              end
    3.12 @@ -1840,7 +1840,7 @@
    3.13                        | inst_type ty1 ty2 (ty as Type(name,tys)) =
    3.14                          Type(name,map (inst_type ty1 ty2) tys)
    3.15                  in
    3.16 -                    foldr (fn (v,th) =>
    3.17 +                    List.foldr (fn (v,th) =>
    3.18                                let
    3.19                                    val cdom = fst (dom_rng (fst (dom_rng cty)))
    3.20                                    val vty  = type_of v
    3.21 @@ -1852,7 +1852,7 @@
    3.22                  end
    3.23                | SOME _ => raise ERR "GEN_ABS" "Bad constant"
    3.24                | NONE =>
    3.25 -                foldr (fn (v,th) => mk_ABS v th thy) th vlist'
    3.26 +                List.foldr (fn (v,th) => mk_ABS v th thy) th vlist'
    3.27          val res = HOLThm(rens_of info',th1)
    3.28          val _ = message "RESULT:"
    3.29          val _ = if_debug pth res
    3.30 @@ -2020,7 +2020,7 @@
    3.31                                 Sign.add_consts_i consts thy'
    3.32                             end
    3.33  
    3.34 -            val thy1 = foldr (fn(name,thy)=>
    3.35 +            val thy1 = List.foldr (fn(name,thy)=>
    3.36                                  snd (get_defname thyname name thy)) thy1 names
    3.37              fun new_name name = fst (get_defname thyname name thy1)
    3.38              val names' = map (fn name => (new_name name,name,false)) names
    3.39 @@ -2041,7 +2041,7 @@
    3.40                       then quotename name
    3.41                       else (quotename newname) ^ ": " ^ (quotename name),thy')
    3.42                  end
    3.43 -            val (new_names,thy') = foldr (fn(name,(names,thy)) =>
    3.44 +            val (new_names,thy') = List.foldr (fn(name,(names,thy)) =>
    3.45                                              let
    3.46                                                  val (name',thy') = handle_const (name,thy)
    3.47                                              in
     4.1 --- a/src/HOL/Nominal/nominal_package.ML	Sun Mar 01 16:48:06 2009 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sun Mar 01 23:36:12 2009 +0100
     4.3 @@ -547,10 +547,10 @@
     4.4                    HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
     4.5                      T --> HOLogic.boolT) $ free')) :: prems
     4.6                | _ => prems,
     4.7 -            snd (foldr mk_abs_fun (j', free) Ts) :: ts)
     4.8 +            snd (List.foldr mk_abs_fun (j', free) Ts) :: ts)
     4.9            end;
    4.10  
    4.11 -        val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs;
    4.12 +        val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs;
    4.13          val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
    4.14            list_comb (Const (cname, map fastype_of ts ---> T), ts))
    4.15        in Logic.list_implies (prems, concl)
    4.16 @@ -716,7 +716,7 @@
    4.17            Type ("Nominal.noption", [U])) $ x $ t
    4.18        end;
    4.19  
    4.20 -    val (ty_idxs, _) = foldl
    4.21 +    val (ty_idxs, _) = List.foldl
    4.22        (fn ((i, ("Nominal.noption", _, _)), p) => p
    4.23          | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
    4.24  
    4.25 @@ -738,7 +738,7 @@
    4.26                 val SOME index = AList.lookup op = ty_idxs i;
    4.27                 val (constrs1, constrs2) = ListPair.unzip
    4.28                   (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
    4.29 -                   (foldl_map (fn (dts, dt) =>
    4.30 +                   (Library.foldl_map (fn (dts, dt) =>
    4.31                       let val (dts', dt') = strip_option dt
    4.32                       in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end)
    4.33                         ([], cargs))) constrs)
    4.34 @@ -780,7 +780,7 @@
    4.35            in
    4.36              (j + length dts + 1,
    4.37               xs @ x :: l_args,
    4.38 -             foldr mk_abs_fun
    4.39 +             List.foldr mk_abs_fun
    4.40                 (case dt of
    4.41                    DtRec k => if k < length new_type_names then
    4.42                        Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
    4.43 @@ -789,7 +789,7 @@
    4.44                  | _ => x) xs :: r_args)
    4.45            end
    4.46  
    4.47 -        val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
    4.48 +        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
    4.49          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
    4.50          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
    4.51          val constrT = map fastype_of l_args ---> T;
    4.52 @@ -909,7 +909,7 @@
    4.53                 map perm (xs @ [x]) @ r_args)
    4.54              end
    4.55  
    4.56 -          val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts;
    4.57 +          val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
    4.58            val c = Const (cname, map fastype_of l_args ---> T)
    4.59          in
    4.60            Goal.prove_global thy8 [] []
    4.61 @@ -958,10 +958,10 @@
    4.62                (j + length dts + 1,
    4.63                 xs @ (x :: args1), ys @ (y :: args2),
    4.64                 HOLogic.mk_eq
    4.65 -                 (foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs)
    4.66 +                 (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs)
    4.67              end;
    4.68  
    4.69 -          val (_, args1, args2, eqs) = foldr make_inj (1, [], [], []) dts;
    4.70 +          val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts;
    4.71            val Ts = map fastype_of args1;
    4.72            val c = Const (cname, Ts ---> T)
    4.73          in
    4.74 @@ -997,10 +997,10 @@
    4.75                val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
    4.76              in
    4.77                (j + length dts + 1,
    4.78 -               xs @ (x :: args1), foldr mk_abs_fun x xs :: args2)
    4.79 +               xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2)
    4.80              end;
    4.81  
    4.82 -          val (_, args1, args2) = foldr process_constr (1, [], []) dts;
    4.83 +          val (_, args1, args2) = List.foldr process_constr (1, [], []) dts;
    4.84            val Ts = map fastype_of args1;
    4.85            val c = list_comb (Const (cname, Ts ---> T), args1);
    4.86            fun supp t =
    4.87 @@ -1413,7 +1413,7 @@
    4.88  
    4.89      val _ = warning "defining recursion combinator ...";
    4.90  
    4.91 -    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
    4.92 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    4.93  
    4.94      val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts used;
    4.95  
     5.1 --- a/src/HOL/Tools/TFL/post.ML	Sun Mar 01 16:48:06 2009 +0100
     5.2 +++ b/src/HOL/Tools/TFL/post.ML	Sun Mar 01 23:36:12 2009 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Tools/TFL/post.ML
     5.5 -    ID:         $Id$
     5.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
     5.7      Copyright   1997  University of Cambridge
     5.8  
     5.9 @@ -31,7 +30,7 @@
    5.10   *--------------------------------------------------------------------------*)
    5.11  fun termination_goals rules =
    5.12      map (Type.freeze o HOLogic.dest_Trueprop)
    5.13 -      (foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
    5.14 +      (List.foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
    5.15  
    5.16  (*---------------------------------------------------------------------------
    5.17   * Finds the termination conditions in (highly massaged) definition and
     6.1 --- a/src/HOL/Tools/TFL/rules.ML	Sun Mar 01 16:48:06 2009 +0100
     6.2 +++ b/src/HOL/Tools/TFL/rules.ML	Sun Mar 01 23:36:12 2009 +0100
     6.3 @@ -131,7 +131,7 @@
     6.4  
     6.5  fun FILTER_DISCH_ALL P thm =
     6.6   let fun check tm = P (#t (Thm.rep_cterm tm))
     6.7 - in  foldr (fn (tm,th) => if check tm then DISCH tm th else th)
     6.8 + in  List.foldr (fn (tm,th) => if check tm then DISCH tm th else th)
     6.9                thm (chyps thm)
    6.10   end;
    6.11  
     7.1 --- a/src/HOL/Tools/TFL/tfl.ML	Sun Mar 01 16:48:06 2009 +0100
     7.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Sun Mar 01 23:36:12 2009 +0100
     7.3 @@ -330,7 +330,7 @@
     7.4       val dummy = map (no_repeat_vars thy) pats
     7.5       val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
     7.6                                map (fn (t,i) => (t,(i,true))) (enumerate R))
     7.7 -     val names = foldr OldTerm.add_term_names [] R
     7.8 +     val names = List.foldr OldTerm.add_term_names [] R
     7.9       val atype = type_of(hd pats)
    7.10       and aname = Name.variant names "a"
    7.11       val a = Free(aname,atype)
    7.12 @@ -492,7 +492,7 @@
    7.13       val tych = Thry.typecheck thy
    7.14       val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
    7.15       val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
    7.16 -     val R = Free (Name.variant (foldr OldTerm.add_term_names [] eqns) Rname,
    7.17 +     val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
    7.18                     Rtype)
    7.19       val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
    7.20       val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
    7.21 @@ -533,7 +533,7 @@
    7.22                         Display.prths extractants;
    7.23                         ())
    7.24                   else ()
    7.25 -     val TCs = foldr (gen_union (op aconv)) [] TCl
    7.26 +     val TCs = List.foldr (gen_union (op aconv)) [] TCl
    7.27       val full_rqt = WFR::TCs
    7.28       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
    7.29       val R'abs = S.rand R'
    7.30 @@ -690,7 +690,7 @@
    7.31   let val tych = Thry.typecheck thy
    7.32       val ty_info = Thry.induct_info thy
    7.33   in fn pats =>
    7.34 - let val names = foldr OldTerm.add_term_names [] pats
    7.35 + let val names = List.foldr OldTerm.add_term_names [] pats
    7.36       val T = type_of (hd pats)
    7.37       val aname = Name.variant names "a"
    7.38       val vname = Name.variant (aname::names) "v"
    7.39 @@ -843,7 +843,7 @@
    7.40      val (pats,TCsl) = ListPair.unzip pat_TCs_list
    7.41      val case_thm = complete_cases thy pats
    7.42      val domain = (type_of o hd) pats
    7.43 -    val Pname = Name.variant (foldr (Library.foldr OldTerm.add_term_names)
    7.44 +    val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names)
    7.45                                [] (pats::TCsl)) "P"
    7.46      val P = Free(Pname, domain --> HOLogic.boolT)
    7.47      val Sinduct = R.SPEC (tych P) Sinduction
    7.48 @@ -854,7 +854,7 @@
    7.49      val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
    7.50      val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
    7.51      val proved_cases = map (prove_case fconst thy) tasks
    7.52 -    val v = Free (Name.variant (foldr OldTerm.add_term_names [] (map concl proved_cases))
    7.53 +    val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases))
    7.54                      "v",
    7.55                    domain)
    7.56      val vtyped = tych v
     8.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Mar 01 16:48:06 2009 +0100
     8.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Mar 01 23:36:12 2009 +0100
     8.3 @@ -96,7 +96,7 @@
     8.4  
     8.5      val descr' = List.concat descr;
     8.6      val recTs = get_rec_types descr' sorts;
     8.7 -    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
     8.8 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
     8.9      val newTs = Library.take (length (hd descr), recTs);
    8.10  
    8.11      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    8.12 @@ -140,7 +140,7 @@
    8.13            end;
    8.14  
    8.15          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    8.16 -        val (_, _, prems, t1s, t2s) = foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
    8.17 +        val (_, _, prems, t1s, t2s) = List.foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
    8.18  
    8.19        in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
    8.20          (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
    8.21 @@ -280,7 +280,7 @@
    8.22  
    8.23      val descr' = List.concat descr;
    8.24      val recTs = get_rec_types descr' sorts;
    8.25 -    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
    8.26 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    8.27      val newTs = Library.take (length (hd descr), recTs);
    8.28      val T' = TFree (Name.variant used "'t", HOLogic.typeS);
    8.29  
     9.1 --- a/src/HOL/Tools/datatype_aux.ML	Sun Mar 01 16:48:06 2009 +0100
     9.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sun Mar 01 23:36:12 2009 +0100
     9.3 @@ -155,7 +155,7 @@
     9.4      val prem' = hd (prems_of exhaustion);
     9.5      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
     9.6      val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
     9.7 -      cterm_of thy (foldr (fn ((_, T), t) => Abs ("z", T, t))
     9.8 +      cterm_of thy (List.foldr (fn ((_, T), t) => Abs ("z", T, t))
     9.9          (Bound 0) params))] exhaustion
    9.10    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    9.11    end;
    10.1 --- a/src/HOL/Tools/datatype_codegen.ML	Sun Mar 01 16:48:06 2009 +0100
    10.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Sun Mar 01 23:36:12 2009 +0100
    10.3 @@ -85,7 +85,7 @@
    10.4              val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
    10.5              val T = Type (tname, dts');
    10.6              val rest = mk_term_of_def gr "and " xs;
    10.7 -            val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) =>
    10.8 +            val (_, eqs) = Library.foldl_map (fn (prfx, (cname, Ts)) =>
    10.9                let val args = map (fn i =>
   10.10                  str ("x" ^ string_of_int i)) (1 upto length Ts)
   10.11                in ("  | ", Pretty.blk (4,
   10.12 @@ -216,8 +216,8 @@
   10.13        let
   10.14          val ts1 = Library.take (i, ts);
   10.15          val t :: ts2 = Library.drop (i, ts);
   10.16 -        val names = foldr OldTerm.add_term_names
   10.17 -          (map (fst o fst o dest_Var) (foldr OldTerm.add_term_vars [] ts1)) ts1;
   10.18 +        val names = List.foldr OldTerm.add_term_names
   10.19 +          (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
   10.20          val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
   10.21  
   10.22          fun pcase [] [] [] gr = ([], gr)
    11.1 --- a/src/HOL/Tools/datatype_prop.ML	Sun Mar 01 16:48:06 2009 +0100
    11.2 +++ b/src/HOL/Tools/datatype_prop.ML	Sun Mar 01 23:36:12 2009 +0100
    11.3 @@ -205,7 +205,7 @@
    11.4    let
    11.5      val descr' = List.concat descr;
    11.6      val recTs = get_rec_types descr' sorts;
    11.7 -    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
    11.8 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    11.9  
   11.10      val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
   11.11  
   11.12 @@ -255,7 +255,7 @@
   11.13    let
   11.14      val descr' = List.concat descr;
   11.15      val recTs = get_rec_types descr' sorts;
   11.16 -    val used = foldr OldTerm.add_typ_tfree_names [] recTs;
   11.17 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   11.18      val newTs = Library.take (length (hd descr), recTs);
   11.19      val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   11.20  
   11.21 @@ -302,7 +302,7 @@
   11.22    let
   11.23      val descr' = List.concat descr;
   11.24      val recTs = get_rec_types descr' sorts;
   11.25 -    val used' = foldr OldTerm.add_typ_tfree_names [] recTs;
   11.26 +    val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   11.27      val newTs = Library.take (length (hd descr), recTs);
   11.28      val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
   11.29      val P = Free ("P", T' --> HOLogic.boolT);
   11.30 @@ -319,13 +319,13 @@
   11.31              val eqn = HOLogic.mk_eq (Free ("x", T),
   11.32                list_comb (Const (cname, Ts ---> T), frees));
   11.33              val P' = P $ list_comb (f, frees)
   11.34 -          in ((foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
   11.35 +          in ((List.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
   11.36                  (HOLogic.imp $ eqn $ P') frees)::t1s,
   11.37 -              (foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
   11.38 +              (List.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
   11.39                  (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s)
   11.40            end;
   11.41  
   11.42 -        val (t1s, t2s) = foldr process_constr ([], []) (constrs ~~ fs);
   11.43 +        val (t1s, t2s) = List.foldr process_constr ([], []) (constrs ~~ fs);
   11.44          val lhs = P $ (comb_t $ Free ("x", T))
   11.45        in
   11.46          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
   11.47 @@ -422,7 +422,7 @@
   11.48          val tnames = Name.variant_list ["v"] (make_tnames Ts);
   11.49          val frees = tnames ~~ Ts
   11.50        in
   11.51 -        foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
   11.52 +        List.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
   11.53            (HOLogic.mk_eq (Free ("v", T),
   11.54              list_comb (Const (cname, Ts ---> T), map Free frees))) frees
   11.55        end
    12.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sun Mar 01 16:48:06 2009 +0100
    12.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sun Mar 01 23:36:12 2009 +0100
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      HOL/Tools/datatype_realizer.ML
    12.5 -    ID:         $Id$
    12.6      Author:     Stefan Berghofer, TU Muenchen
    12.7  
    12.8  Porgram extraction from proofs involving datatypes:
    12.9 @@ -57,8 +56,8 @@
   12.10      fun mk_all i s T t =
   12.11        if i mem is then list_all_free ([(s, T)], t) else t;
   12.12  
   12.13 -    val (prems, rec_fns) = split_list (List.concat (snd (foldl_map
   12.14 -      (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) =>
   12.15 +    val (prems, rec_fns) = split_list (List.concat (snd (Library.foldl_map
   12.16 +      (fn (j, ((i, (_, _, constrs)), T)) => Library.foldl_map (fn (j, (cname, cargs)) =>
   12.17          let
   12.18            val Ts = map (typ_of_dtyp descr sorts) cargs;
   12.19            val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
   12.20 @@ -139,8 +138,8 @@
   12.21        tname_of (body_type T) mem ["set", "bool"]) ivs);
   12.22      val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
   12.23  
   12.24 -    val prf = foldr forall_intr_prf
   12.25 -     (foldr (fn ((f, p), prf) =>
   12.26 +    val prf = List.foldr forall_intr_prf
   12.27 +     (List.foldr (fn ((f, p), prf) =>
   12.28          (case head_of (strip_abs_body f) of
   12.29             Free (s, T) =>
   12.30               let val T' = Logic.varifyT T
   12.31 @@ -151,7 +150,7 @@
   12.32             (Proofterm.proof_combP
   12.33               (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2;
   12.34  
   12.35 -    val r' = if null is then r else Logic.varify (foldr (uncurry lambda)
   12.36 +    val r' = if null is then r else Logic.varify (List.foldr (uncurry lambda)
   12.37        r (map Logic.unvarify ivs1 @ filter_out is_unit
   12.38            (map (head_of o strip_abs_body) rec_fns)));
   12.39  
   12.40 @@ -201,7 +200,7 @@
   12.41  
   12.42      val P = Var (("P", 0), rT' --> HOLogic.boolT);
   12.43      val prf = forall_intr_prf (y, forall_intr_prf (P,
   12.44 -      foldr (fn ((p, r), prf) =>
   12.45 +      List.foldr (fn ((p, r), prf) =>
   12.46          forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p),
   12.47            prf))) (Proofterm.proof_combP (prf_of thm',
   12.48              map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
    13.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Mar 01 16:48:06 2009 +0100
    13.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Mar 01 23:36:12 2009 +0100
    13.3 @@ -83,7 +83,7 @@
    13.4      val branchT = if null branchTs then HOLogic.unitT
    13.5        else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
    13.6      val arities = get_arities descr' \ 0;
    13.7 -    val unneeded_vars = hd tyvars \\ foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
    13.8 +    val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
    13.9      val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
   13.10      val recTs = get_rec_types descr' sorts;
   13.11      val newTs = Library.take (length (hd descr), recTs);
   13.12 @@ -143,7 +143,7 @@
   13.13        in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
   13.14        end;
   13.15  
   13.16 -    val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
   13.17 +    val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
   13.18  
   13.19      (************** generate introduction rules for representing set **********)
   13.20  
   13.21 @@ -169,7 +169,7 @@
   13.22                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
   13.23                end);
   13.24  
   13.25 -        val (_, prems, ts) = foldr mk_prem (1, [], []) cargs;
   13.26 +        val (_, prems, ts) = List.foldr mk_prem (1, [], []) cargs;
   13.27          val concl = HOLogic.mk_Trueprop
   13.28            (Free (s, UnivT') $ mk_univ_inj ts n i)
   13.29        in Logic.list_implies (prems, concl)
   13.30 @@ -229,7 +229,7 @@
   13.31              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
   13.32            end;
   13.33  
   13.34 -        val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
   13.35 +        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
   13.36          val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
   13.37          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
   13.38          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
   13.39 @@ -357,7 +357,7 @@
   13.40  
   13.41        in (thy', char_thms' @ char_thms) end;
   13.42  
   13.43 -    val (thy5, iso_char_thms) = apfst Theory.checkpoint (foldr make_iso_defs
   13.44 +    val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
   13.45        (add_path flat_names big_name thy4, []) (tl descr));
   13.46  
   13.47      (* prove isomorphism properties *)
   13.48 @@ -447,7 +447,7 @@
   13.49        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
   13.50        end;
   13.51  
   13.52 -    val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
   13.53 +    val (iso_inj_thms_unfolded, iso_elem_thms) = List.foldr prove_iso_thms
   13.54        ([], map #3 newT_iso_axms) (tl descr);
   13.55      val iso_inj_thms = map snd newT_iso_inj_thms @
   13.56        map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
    14.1 --- a/src/HOL/Tools/function_package/scnp_solve.ML	Sun Mar 01 16:48:06 2009 +0100
    14.2 +++ b/src/HOL/Tools/function_package/scnp_solve.ML	Sun Mar 01 23:36:12 2009 +0100
    14.3 @@ -46,7 +46,7 @@
    14.4  fun num_prog_pts (GP (arities, _)) = length arities ;
    14.5  fun num_graphs (GP (_, gs)) = length gs ;
    14.6  fun arity (GP (arities, gl)) i = nth arities i ;
    14.7 -fun ndigits (GP (arities, _)) = IntInf.log2 (foldl (op +) 0 arities) + 1
    14.8 +fun ndigits (GP (arities, _)) = IntInf.log2 (List.foldl (op +) 0 arities) + 1
    14.9  
   14.10  
   14.11  (** Propositional formulas **)
   14.12 @@ -79,7 +79,7 @@
   14.13  fun var_constrs (gp as GP (arities, gl)) =
   14.14    let
   14.15      val n = Int.max (num_graphs gp, num_prog_pts gp)
   14.16 -    val k = foldl Int.max 1 arities
   14.17 +    val k = List.foldl Int.max 1 arities
   14.18  
   14.19      (* Injective, provided  a < 8, x < n, and i < k. *)
   14.20      fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
    15.1 --- a/src/HOL/Tools/function_package/size.ML	Sun Mar 01 16:48:06 2009 +0100
    15.2 +++ b/src/HOL/Tools/function_package/size.ML	Sun Mar 01 23:36:12 2009 +0100
    15.3 @@ -115,7 +115,7 @@
    15.4            then HOLogic.zero
    15.5            else foldl1 plus (ts @ [HOLogic.Suc_zero])
    15.6        in
    15.7 -        foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
    15.8 +        List.foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
    15.9        end;
   15.10  
   15.11      val fs = maps (fn (_, (name, _, constrs)) =>
    16.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun Mar 01 16:48:06 2009 +0100
    16.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sun Mar 01 23:36:12 2009 +0100
    16.3 @@ -71,7 +71,7 @@
    16.4            {intros = intros |>
    16.5             Symtab.update (s, (AList.update Thm.eq_thm_prop
    16.6               (thm, (thyname_of s, nparms)) rules)),
    16.7 -           graph = foldr (uncurry (Graph.add_edge o pair s))
    16.8 +           graph = List.foldr (uncurry (Graph.add_edge o pair s))
    16.9               (Library.foldl add_node (graph, s :: cs)) cs,
   16.10             eqns = eqns} thy
   16.11          end
   16.12 @@ -152,7 +152,7 @@
   16.13  fun cprod ([], ys) = []
   16.14    | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
   16.15  
   16.16 -fun cprods xss = foldr (map op :: o cprod) [[]] xss;
   16.17 +fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
   16.18  
   16.19  datatype mode = Mode of (int list option list * int list) * int list * mode option list;
   16.20  
   16.21 @@ -357,7 +357,7 @@
   16.22  
   16.23      val (in_ts, out_ts) = get_args is 1 ts;
   16.24      val ((all_vs', eqs), in_ts') =
   16.25 -      foldl_map check_constrt ((all_vs, []), in_ts);
   16.26 +      Library.foldl_map check_constrt ((all_vs, []), in_ts);
   16.27  
   16.28      fun compile_prems out_ts' vs names [] gr =
   16.29            let
   16.30 @@ -365,8 +365,8 @@
   16.31                (invoke_codegen thy defs dep module false) out_ts gr;
   16.32              val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
   16.33              val ((names', eqs'), out_ts'') =
   16.34 -              foldl_map check_constrt ((names, []), out_ts');
   16.35 -            val (nvs, out_ts''') = foldl_map distinct_v
   16.36 +              Library.foldl_map check_constrt ((names, []), out_ts');
   16.37 +            val (nvs, out_ts''') = Library.foldl_map distinct_v
   16.38                ((names', map (fn x => (x, [x])) vs), out_ts'');
   16.39              val (out_ps', gr4) = fold_map
   16.40                (invoke_codegen thy defs dep module false) (out_ts''') gr3;
   16.41 @@ -383,8 +383,8 @@
   16.42                select_mode_prem thy modes' vs' ps;
   16.43              val ps' = filter_out (equal p) ps;
   16.44              val ((names', eqs), out_ts') =
   16.45 -              foldl_map check_constrt ((names, []), out_ts);
   16.46 -            val (nvs, out_ts'') = foldl_map distinct_v
   16.47 +              Library.foldl_map check_constrt ((names, []), out_ts);
   16.48 +            val (nvs, out_ts'') = Library.foldl_map distinct_v
   16.49                ((names', map (fn x => (x, [x])) vs), out_ts');
   16.50              val (out_ps, gr0) = fold_map
   16.51                (invoke_codegen thy defs dep module false) out_ts'' gr;
    17.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Mar 01 16:48:06 2009 +0100
    17.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Mar 01 23:36:12 2009 +0100
    17.3 @@ -517,7 +517,7 @@
    17.4            (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
    17.5  
    17.6        in list_all_free (Logic.strip_params r,
    17.7 -        Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
    17.8 +        Logic.list_implies (map HOLogic.mk_Trueprop (List.foldr mk_prem
    17.9            [] (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r))),
   17.10              HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
   17.11        end;
   17.12 @@ -541,7 +541,7 @@
   17.13      (* make predicate for instantiation of abstract induction rule *)
   17.14  
   17.15      val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
   17.16 -      (map_index (fn (i, P) => foldr HOLogic.mk_imp
   17.17 +      (map_index (fn (i, P) => List.foldr HOLogic.mk_imp
   17.18           (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))
   17.19           (make_bool_args HOLogic.mk_not I bs i)) preds));
   17.20  
   17.21 @@ -624,7 +624,7 @@
   17.22            map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
   17.23            map (subst o HOLogic.dest_Trueprop)
   17.24              (Logic.strip_assums_hyp r)
   17.25 -      in foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
   17.26 +      in List.foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
   17.27          (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
   17.28          (Logic.strip_params r)
   17.29        end
    18.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Mar 01 16:48:06 2009 +0100
    18.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Mar 01 23:36:12 2009 +0100
    18.3 @@ -55,7 +55,7 @@
    18.4        (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
    18.5    | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
    18.6  
    18.7 -fun relevant_vars prop = foldr (fn
    18.8 +fun relevant_vars prop = List.foldr (fn
    18.9        (Var ((a, i), T), vs) => (case strip_type T of
   18.10          (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
   18.11        | _ => vs)
   18.12 @@ -264,7 +264,7 @@
   18.13      val rlz'' = fold_rev Logic.all vs2 rlz
   18.14    in (name, (vs,
   18.15      if rt = Extraction.nullt then rt else
   18.16 -      foldr (uncurry lambda) rt vs1,
   18.17 +      List.foldr (uncurry lambda) rt vs1,
   18.18      ProofRewriteRules.un_hhf_proof rlz' rlz''
   18.19        (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
   18.20    end;
   18.21 @@ -315,7 +315,7 @@
   18.22      fun get f = (these oo Option.map) f;
   18.23      val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
   18.24        HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
   18.25 -    val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
   18.26 +    val (_, constrss) = Library.foldl_map (fn ((recs, dummies), (s, rs)) =>
   18.27        if s mem rsets then
   18.28          let
   18.29            val (d :: dummies') = dummies;
    19.1 --- a/src/HOL/Tools/lin_arith.ML	Sun Mar 01 16:48:06 2009 +0100
    19.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 01 23:36:12 2009 +0100
    19.3 @@ -672,7 +672,7 @@
    19.4  let
    19.5    fun filter_prems (t, (left, right)) =
    19.6      if  p t  then  (left, right @ [t])  else  (left @ right, [])
    19.7 -  val (left, right) = foldl filter_prems ([], []) terms
    19.8 +  val (left, right) = List.foldl filter_prems ([], []) terms
    19.9  in
   19.10    right @ left
   19.11  end;
    20.1 --- a/src/HOL/Tools/meson.ML	Sun Mar 01 16:48:06 2009 +0100
    20.2 +++ b/src/HOL/Tools/meson.ML	Sun Mar 01 23:36:12 2009 +0100
    20.3 @@ -92,7 +92,7 @@
    20.4      | pairs =>
    20.5          let val thy = theory_of_thm th
    20.6              val (tyenv,tenv) =
    20.7 -                  foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
    20.8 +                  List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
    20.9              val t_pairs = map term_pair_of (Vartab.dest tenv)
   20.10              val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
   20.11          in  th'  end
   20.12 @@ -428,7 +428,7 @@
   20.13  fun name_thms label =
   20.14      let fun name1 (th, (k,ths)) =
   20.15            (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
   20.16 -    in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
   20.17 +    in  fn ths => #2 (List.foldr name1 (length ths, []) ths)  end;
   20.18  
   20.19  (*Is the given disjunction an all-negative support clause?*)
   20.20  fun is_negative th = forall (not o #1) (literals (prop_of th));
   20.21 @@ -477,7 +477,7 @@
   20.22  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   20.23  fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   20.24  
   20.25 -fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
   20.26 +fun size_of_subgoals st = List.foldr addconcl 0 (prems_of st);
   20.27  
   20.28  
   20.29  (*Negation Normal Form*)
   20.30 @@ -544,12 +544,12 @@
   20.31  
   20.32  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   20.33    The resulting clauses are HOL disjunctions.*)
   20.34 -fun make_clauses ths = sort_clauses (foldr add_clauses [] ths);
   20.35 +fun make_clauses ths = sort_clauses (List.foldr add_clauses [] ths);
   20.36  
   20.37  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   20.38  fun make_horns ths =
   20.39      name_thms "Horn#"
   20.40 -      (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
   20.41 +      (distinct Thm.eq_thm_prop (List.foldr (add_contras clause_rules) [] ths));
   20.42  
   20.43  (*Could simply use nprems_of, which would count remaining subgoals -- no
   20.44    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
    21.1 --- a/src/HOL/Tools/metis_tools.ML	Sun Mar 01 16:48:06 2009 +0100
    21.2 +++ b/src/HOL/Tools/metis_tools.ML	Sun Mar 01 23:36:12 2009 +0100
    21.3 @@ -543,9 +543,9 @@
    21.4          val all_thms_FO = forall (Meson.is_fol_term thy o prop_of)
    21.5          val isFO = (mode = ResAtp.Fol) orelse
    21.6                     (mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths))
    21.7 -        val lmap0 = foldl (add_thm true ctxt)
    21.8 +        val lmap0 = List.foldl (add_thm true ctxt)
    21.9                            {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls
   21.10 -        val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths
   21.11 +        val lmap = List.foldl (add_thm false ctxt) (add_tfrees lmap0) ths
   21.12          val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   21.13          fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
   21.14          (*Now check for the existence of certain combinators*)
   21.15 @@ -556,7 +556,7 @@
   21.16          val thS   = if used "c_COMBS" then [comb_S] else []
   21.17          val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
   21.18          val lmap' = if isFO then lmap
   21.19 -                    else foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
   21.20 +                    else List.foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
   21.21      in
   21.22          add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
   21.23      end;
    22.1 --- a/src/HOL/Tools/old_primrec_package.ML	Sun Mar 01 16:48:06 2009 +0100
    22.2 +++ b/src/HOL/Tools/old_primrec_package.ML	Sun Mar 01 23:36:12 2009 +0100
    22.3 @@ -37,8 +37,8 @@
    22.4      fun varify (t, (i, ts)) =
    22.5        let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
    22.6        in (maxidx_of_term t', t'::ts) end;
    22.7 -    val (i, cs') = foldr varify (~1, []) cs;
    22.8 -    val (i', intr_ts') = foldr varify (i, []) intr_ts;
    22.9 +    val (i, cs') = List.foldr varify (~1, []) cs;
   22.10 +    val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
   22.11      val rec_consts = fold Term.add_consts cs' [];
   22.12      val intr_consts = fold Term.add_consts intr_ts' [];
   22.13      fun unify (cname, cT) =
    23.1 --- a/src/HOL/Tools/recfun_codegen.ML	Sun Mar 01 16:48:06 2009 +0100
    23.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Sun Mar 01 23:36:12 2009 +0100
    23.3 @@ -143,7 +143,7 @@
    23.4                   val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
    23.5                   val (fundef', gr3) = mk_fundef module' "" true eqs''
    23.6                     (add_edge (dname, dep)
    23.7 -                     (foldr (uncurry new_node) (del_nodes xs gr2)
    23.8 +                     (List.foldr (uncurry new_node) (del_nodes xs gr2)
    23.9                         (map (fn k =>
   23.10                           (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
   23.11                 in (module', put_code module' fundef' gr3) end
    24.1 --- a/src/HOL/Tools/record_package.ML	Sun Mar 01 16:48:06 2009 +0100
    24.2 +++ b/src/HOL/Tools/record_package.ML	Sun Mar 01 23:36:12 2009 +0100
    24.3 @@ -1778,7 +1778,7 @@
    24.4      val names = map fst fields;
    24.5      val extN = full bname;
    24.6      val types = map snd fields;
    24.7 -    val alphas_fields = foldr OldTerm.add_typ_tfree_names [] types;
    24.8 +    val alphas_fields = List.foldr OldTerm.add_typ_tfree_names [] types;
    24.9      val alphas_ext = alphas inter alphas_fields;
   24.10      val len = length fields;
   24.11      val variants = Name.variant_list (moreN::rN::rN ^ "'"::wN::parent_variants) (map fst bfields);
   24.12 @@ -1835,7 +1835,7 @@
   24.13        let val (args',more) = chop_last args;
   24.14            fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
   24.15            fun build Ts =
   24.16 -           foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')))
   24.17 +           List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')))
   24.18        in
   24.19          if more = HOLogic.unit
   24.20          then build (map recT (0 upto parent_len))
   24.21 @@ -2003,13 +2003,13 @@
   24.22        end;
   24.23  
   24.24      val split_object_prop =
   24.25 -      let fun ALL vs t = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs
   24.26 +      let fun ALL vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs
   24.27        in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0))
   24.28        end;
   24.29  
   24.30  
   24.31      val split_ex_prop =
   24.32 -      let fun EX vs t = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) t vs
   24.33 +      let fun EX vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) t vs
   24.34        in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0))
   24.35        end;
   24.36  
   24.37 @@ -2228,7 +2228,7 @@
   24.38      val init_env =
   24.39        (case parent of
   24.40          NONE => []
   24.41 -      | SOME (types, _) => foldr OldTerm.add_typ_tfrees [] types);
   24.42 +      | SOME (types, _) => List.foldr OldTerm.add_typ_tfrees [] types);
   24.43  
   24.44  
   24.45      (* fields *)
    25.1 --- a/src/HOL/Tools/refute.ML	Sun Mar 01 16:48:06 2009 +0100
    25.2 +++ b/src/HOL/Tools/refute.ML	Sun Mar 01 23:36:12 2009 +0100
    25.3 @@ -985,7 +985,7 @@
    25.4                  DatatypeAux.DtTFree _ =>
    25.5                  collect_types dT acc
    25.6                | DatatypeAux.DtType (_, ds) =>
    25.7 -                collect_types dT (foldr collect_dtyp acc ds)
    25.8 +                collect_types dT (List.foldr collect_dtyp acc ds)
    25.9                | DatatypeAux.DtRec i =>
   25.10                  if dT mem acc then
   25.11                    acc  (* prevent infinite recursion *)
   25.12 @@ -999,9 +999,9 @@
   25.13                          insert (op =) dT acc
   25.14                        else acc
   25.15                      (* collect argument types *)
   25.16 -                    val acc_dtyps = foldr collect_dtyp acc_dT dtyps
   25.17 +                    val acc_dtyps = List.foldr collect_dtyp acc_dT dtyps
   25.18                      (* collect constructor types *)
   25.19 -                    val acc_dconstrs = foldr collect_dtyp acc_dtyps
   25.20 +                    val acc_dconstrs = List.foldr collect_dtyp acc_dtyps
   25.21                        (List.concat (map snd dconstrs))
   25.22                    in
   25.23                      acc_dconstrs
   25.24 @@ -1102,7 +1102,7 @@
   25.25      case next (maxsize-minsize) 0 0 diffs of
   25.26        SOME diffs' =>
   25.27        (* merge with those types for which the size is fixed *)
   25.28 -      SOME (snd (foldl_map (fn (ds, (T, _)) =>
   25.29 +      SOME (snd (Library.foldl_map (fn (ds, (T, _)) =>
   25.30          case AList.lookup (op =) sizes (string_of_typ T) of
   25.31          (* return the fixed size *)
   25.32            SOME n => (ds, (T, n))
   25.33 @@ -1196,7 +1196,7 @@
   25.34          val _          = Output.immediate_output ("Translating term (sizes: "
   25.35            ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
   25.36          (* translate 'u' and all axioms *)
   25.37 -        val ((model, args), intrs) = foldl_map (fn ((m, a), t') =>
   25.38 +        val ((model, args), intrs) = Library.foldl_map (fn ((m, a), t') =>
   25.39            let
   25.40              val (i, m', a') = interpret thy m a t'
   25.41            in
   25.42 @@ -1612,7 +1612,7 @@
   25.43      val Ts = Term.binder_types (Term.fastype_of t)
   25.44      val t' = Term.incr_boundvars i t
   25.45    in
   25.46 -    foldr (fn (T, term) => Abs ("<eta_expand>", T, term))
   25.47 +    List.foldr (fn (T, term) => Abs ("<eta_expand>", T, term))
   25.48        (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i))
   25.49    end;
   25.50  
   25.51 @@ -1622,7 +1622,7 @@
   25.52  
   25.53    (* int list -> int *)
   25.54  
   25.55 -  fun sum xs = foldl op+ 0 xs;
   25.56 +  fun sum xs = List.foldl op+ 0 xs;
   25.57  
   25.58  (* ------------------------------------------------------------------------- *)
   25.59  (* product: returns the product of a list 'xs' of integers                   *)
   25.60 @@ -1630,7 +1630,7 @@
   25.61  
   25.62    (* int list -> int *)
   25.63  
   25.64 -  fun product xs = foldl op* 1 xs;
   25.65 +  fun product xs = List.foldl op* 1 xs;
   25.66  
   25.67  (* ------------------------------------------------------------------------- *)
   25.68  (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
   25.69 @@ -1750,7 +1750,7 @@
   25.70            (* create all constants of type 'T' *)
   25.71            val constants = make_constants thy model T
   25.72            (* interpret the 'body' separately for each constant *)
   25.73 -          val ((model', args'), bodies) = foldl_map
   25.74 +          val ((model', args'), bodies) = Library.foldl_map
   25.75              (fn ((m, a), c) =>
   25.76                let
   25.77                  (* add 'c' to 'bounds' *)
   25.78 @@ -2094,7 +2094,7 @@
   25.79              Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
   25.80          in
   25.81            (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *)
   25.82 -          map (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
   25.83 +          map (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
   25.84              HOLogic_empty_set) pairss
   25.85          end
   25.86        | Type (s, Ts) =>
   25.87 @@ -2286,7 +2286,7 @@
   25.88                              | search [] _ = ()
   25.89                          in  search terms' terms  end
   25.90                        (* int * interpretation list *)
   25.91 -                      val (new_offset, intrs) = foldl_map (fn (off, t_elem) =>
   25.92 +                      val (new_offset, intrs) = Library.foldl_map (fn (off, t_elem) =>
   25.93                          (* if 't_elem' existed at the previous depth,    *)
   25.94                          (* proceed recursively, otherwise map the entire *)
   25.95                          (* subtree to "undefined"                        *)
   25.96 @@ -2352,7 +2352,7 @@
   25.97                else  (* mconstrs_count = length params *)
   25.98                  let
   25.99                    (* interpret each parameter separately *)
  25.100 -                  val ((model', args'), p_intrs) = foldl_map (fn ((m, a), p) =>
  25.101 +                  val ((model', args'), p_intrs) = Library.foldl_map (fn ((m, a), p) =>
  25.102                      let
  25.103                        val (i, m', a') = interpret thy m a p
  25.104                      in
  25.105 @@ -2464,7 +2464,7 @@
  25.106                      end) descr
  25.107                    (* associate constructors with corresponding parameters *)
  25.108                    (* (int * (interpretation * interpretation) list) list *)
  25.109 -                  val (p_intrs', mc_p_intrs) = foldl_map
  25.110 +                  val (p_intrs', mc_p_intrs) = Library.foldl_map
  25.111                      (fn (p_intrs', (idx, c_intrs)) =>
  25.112                        let
  25.113                          val len = length c_intrs
  25.114 @@ -2630,7 +2630,7 @@
  25.115                          (* interpretation list *)
  25.116                          val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs
  25.117                          (* apply 'intr' to all recursive arguments *)
  25.118 -                        val result = foldl (fn (arg_i, i) =>
  25.119 +                        val result = List.foldl (fn (arg_i, i) =>
  25.120                            interpretation_apply (i, arg_i)) intr arg_intrs
  25.121                          (* update 'REC_OPERATORS' *)
  25.122                          val _ = Array.update (arr, elem, (true, result))
  25.123 @@ -2910,7 +2910,7 @@
  25.124          (* of width 'size_elem' and depth 'length_list' (with 'size_list'    *)
  25.125          (* nodes total)                                                      *)
  25.126          (* (int * (int * int)) list *)
  25.127 -        val (_, lenoff_lists) = foldl_map (fn ((offsets, off), elem) =>
  25.128 +        val (_, lenoff_lists) = Library.foldl_map (fn ((offsets, off), elem) =>
  25.129            (* corresponds to a pre-order traversal of the tree *)
  25.130            let
  25.131              val len = length offsets
  25.132 @@ -3004,7 +3004,7 @@
  25.133              "intersection: interpretation for set is not a node")
  25.134          (* interpretation -> interpretaion *)
  25.135          fun lfp (Node resultsets) =
  25.136 -          foldl (fn ((set, resultset), acc) =>
  25.137 +          List.foldl (fn ((set, resultset), acc) =>
  25.138              if is_subset (resultset, set) then
  25.139                intersection (acc, set)
  25.140              else
  25.141 @@ -3055,7 +3055,7 @@
  25.142              "union: interpretation for set is not a node")
  25.143          (* interpretation -> interpretaion *)
  25.144          fun gfp (Node resultsets) =
  25.145 -          foldl (fn ((set, resultset), acc) =>
  25.146 +          List.foldl (fn ((set, resultset), acc) =>
  25.147              if is_subset (set, resultset) then
  25.148                union (acc, set)
  25.149              else
  25.150 @@ -3158,7 +3158,7 @@
  25.151          val HOLogic_insert    =
  25.152            Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
  25.153        in
  25.154 -        SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
  25.155 +        SOME (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
  25.156            HOLogic_empty_set pairs)
  25.157        end
  25.158      | Type ("prop", [])      =>
  25.159 @@ -3293,8 +3293,6 @@
  25.160  (*       subterms that are then passed to other interpreters!                *)
  25.161  (* ------------------------------------------------------------------------- *)
  25.162  
  25.163 -  (* (theory -> theory) list *)
  25.164 -
  25.165    val setup =
  25.166       add_interpreter "stlc"    stlc_interpreter #>
  25.167       add_interpreter "Pure"    Pure_interpreter #>
    26.1 --- a/src/HOL/Tools/res_atp.ML	Sun Mar 01 16:48:06 2009 +0100
    26.2 +++ b/src/HOL/Tools/res_atp.ML	Sun Mar 01 23:36:12 2009 +0100
    26.3 @@ -115,9 +115,9 @@
    26.4  fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
    26.5  
    26.6  val null_const_tab : const_typ list list Symtab.table = 
    26.7 -    foldl add_standard_const Symtab.empty standard_consts;
    26.8 +    List.foldl add_standard_const Symtab.empty standard_consts;
    26.9  
   26.10 -fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab;
   26.11 +fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab;
   26.12  
   26.13  (*Inserts a dummy "constant" referring to the theory name, so that relevance
   26.14    takes the given theory into account.*)
   26.15 @@ -190,7 +190,7 @@
   26.16      end;
   26.17      
   26.18  (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
   26.19 -fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys;
   26.20 +fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
   26.21  
   26.22  fun consts_typs_of_term thy t = 
   26.23    let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
   26.24 @@ -250,7 +250,7 @@
   26.25  	| relevant (newpairs,rejects) [] =
   26.26  	    let val (newrels,more_rejects) = take_best max_new newpairs
   26.27  		val new_consts = List.concat (map #2 newrels)
   26.28 -		val rel_consts' = foldl add_const_typ_table rel_consts new_consts
   26.29 +		val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
   26.30  		val newp = p + (1.0-p) / convergence
   26.31  	    in
   26.32                Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
   26.33 @@ -376,7 +376,7 @@
   26.34  
   26.35  fun add_single_names ((a, []), pairs) = pairs
   26.36    | add_single_names ((a, [th]), pairs) = (a,th)::pairs
   26.37 -  | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   26.38 +  | add_single_names ((a, ths), pairs) = #2 (List.foldl (multi_name a) (1,pairs) ths);
   26.39  
   26.40  (*Ignore blacklisted basenames*)
   26.41  fun add_multi_names ((a, ths), pairs) =
   26.42 @@ -393,7 +393,7 @@
   26.43    in
   26.44        app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
   26.45        filter (not o blacklisted o #2)
   26.46 -        (foldl add_single_names (foldl add_multi_names [] mults) singles)
   26.47 +        (List.foldl add_single_names (List.foldl add_multi_names [] mults) singles)
   26.48    end;
   26.49  
   26.50  fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
   26.51 @@ -431,18 +431,18 @@
   26.52  (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   26.53  (***************************************************************)
   26.54  
   26.55 -fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
   26.56 +fun add_classes (sorts, cset) = List.foldl setinsert cset (List.concat sorts);
   26.57  
   26.58  (*Remove this trivial type class*)
   26.59  fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
   26.60  
   26.61  fun tvar_classes_of_terms ts =
   26.62    let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   26.63 -  in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   26.64 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   26.65  
   26.66  fun tfree_classes_of_terms ts =
   26.67    let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   26.68 -  in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
   26.69 +  in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   26.70  
   26.71  (*fold type constructors*)
   26.72  fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
    27.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Mar 01 16:48:06 2009 +0100
    27.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 01 23:36:12 2009 +0100
    27.3 @@ -494,7 +494,7 @@
    27.4        val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
    27.5                                        (map Thm.term_of hyps)
    27.6        val fixed = OldTerm.term_frees (concl_of st) @
    27.7 -                  foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
    27.8 +                  List.foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
    27.9    in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
   27.10  
   27.11  
    28.1 --- a/src/HOL/Tools/res_clause.ML	Sun Mar 01 16:48:06 2009 +0100
    28.2 +++ b/src/HOL/Tools/res_clause.ML	Sun Mar 01 23:36:12 2009 +0100
    28.3 @@ -1,5 +1,4 @@
    28.4  (*  Author: Jia Meng, Cambridge University Computer Laboratory
    28.5 -    ID: $Id$
    28.6      Copyright 2004 University of Cambridge
    28.7  
    28.8  Storing/printing FOL clauses and arity clauses.
    28.9 @@ -95,7 +94,7 @@
   28.10  val tconst_prefix = "tc_";
   28.11  val class_prefix = "class_";
   28.12  
   28.13 -fun union_all xss = foldl (op union) [] xss;
   28.14 +fun union_all xss = List.foldl (op union) [] xss;
   28.15  
   28.16  (*Provide readable names for the more common symbolic functions*)
   28.17  val const_trans_table =
   28.18 @@ -275,7 +274,7 @@
   28.19    | pred_of_sort (LTFree (s,ty)) = (s,1)
   28.20  
   28.21  (*Given a list of sorted type variables, return a list of type literals.*)
   28.22 -fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts);
   28.23 +fun add_typs Ts = List.foldl (op union) [] (map sorts_on_typs Ts);
   28.24  
   28.25  (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   28.26    * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
   28.27 @@ -338,8 +337,8 @@
   28.28        let val class_less = Sorts.class_less(Sign.classes_of thy)
   28.29            fun add_super sub (super,pairs) =
   28.30                  if class_less (sub,super) then (sub,super)::pairs else pairs
   28.31 -          fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers
   28.32 -      in  foldl add_supers [] subs  end;
   28.33 +          fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers
   28.34 +      in  List.foldl add_supers [] subs  end;
   28.35  
   28.36  fun make_classrelClause (sub,super) =
   28.37    ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
   28.38 @@ -375,7 +374,7 @@
   28.39        fun add_class tycon (class,pairs) =
   28.40              (class, domain_sorts(tycon,class))::pairs
   28.41              handle Sorts.CLASS_ERROR _ => pairs
   28.42 -      fun try_classes tycon = (tycon, foldl (add_class tycon) [] classes)
   28.43 +      fun try_classes tycon = (tycon, List.foldl (add_class tycon) [] classes)
   28.44    in  map try_classes tycons  end;
   28.45  
   28.46  (*Proving one (tycon, class) membership may require proving others, so iterate.*)
   28.47 @@ -398,7 +397,7 @@
   28.48  (*FIXME: multiple-arity checking doesn't work, as update_new is the wrong
   28.49    function (it flags repeated declarations of a function, even with the same arity)*)
   28.50  
   28.51 -fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs;
   28.52 +fun update_many (tab, keypairs) = List.foldl (uncurry Symtab.update) tab keypairs;
   28.53  
   28.54  fun add_type_sort_preds (T, preds) =
   28.55        update_many (preds, map pred_of_sort (sorts_on_typs T));
   28.56 @@ -412,14 +411,14 @@
   28.57  fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
   28.58    let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits)
   28.59        fun upd (class,preds) = Symtab.update (class,1) preds
   28.60 -  in  foldl upd preds classes  end;
   28.61 +  in  List.foldl upd preds classes  end;
   28.62  
   28.63  (*** Find occurrences of functions in clauses ***)
   28.64  
   28.65  fun add_foltype_funcs (AtomV _, funcs) = funcs
   28.66    | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs
   28.67    | add_foltype_funcs (Comp(a,tys), funcs) =
   28.68 -      foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   28.69 +      List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   28.70  
   28.71  (*TFrees are recorded as constants*)
   28.72  fun add_type_sort_funcs (TVar _, funcs) = funcs
    29.1 --- a/src/HOL/Tools/res_hol_clause.ML	Sun Mar 01 16:48:06 2009 +0100
    29.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Sun Mar 01 23:36:12 2009 +0100
    29.3 @@ -1,4 +1,4 @@
    29.4 -(* ID: $Id$
    29.5 +(*
    29.6     Author: Jia Meng, NICTA
    29.7  
    29.8  FOL clauses translated from HOL formulae.
    29.9 @@ -183,7 +183,7 @@
   29.10        if isTaut cls then pairs else (name,cls)::pairs
   29.11    end;
   29.12  
   29.13 -fun make_axiom_clauses dfg thy = foldl (add_axiom_clause dfg thy) [];
   29.14 +fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) [];
   29.15  
   29.16  fun make_conjecture_clauses_aux dfg _ _ [] = []
   29.17    | make_conjecture_clauses_aux dfg thy n (th::ths) =
   29.18 @@ -328,7 +328,7 @@
   29.19  
   29.20  (** For DFG format: accumulate function and predicate declarations **)
   29.21  
   29.22 -fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars;
   29.23 +fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
   29.24  
   29.25  fun add_decls cma cnh (CombConst(c,tp,tvars), (funcs,preds)) =
   29.26        if c = "equal" then (addtypes tvars funcs, preds)
   29.27 @@ -347,28 +347,28 @@
   29.28  fun add_literal_decls cma cnh (Literal(_,c), decls) = add_decls cma cnh (c,decls);
   29.29  
   29.30  fun add_clause_decls cma cnh (Clause {literals, ...}, decls) =
   29.31 -    foldl (add_literal_decls cma cnh) decls literals
   29.32 +    List.foldl (add_literal_decls cma cnh) decls literals
   29.33      handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
   29.34  
   29.35  fun decls_of_clauses cma cnh clauses arity_clauses =
   29.36    let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
   29.37        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   29.38 -      val (functab,predtab) = (foldl (add_clause_decls cma cnh) (init_functab, init_predtab) clauses)
   29.39 +      val (functab,predtab) = (List.foldl (add_clause_decls cma cnh) (init_functab, init_predtab) clauses)
   29.40    in
   29.41 -      (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses),
   29.42 +      (Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses),
   29.43         Symtab.dest predtab)
   29.44    end;
   29.45  
   29.46  fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
   29.47 -  foldl RC.add_type_sort_preds preds ctypes_sorts
   29.48 +  List.foldl RC.add_type_sort_preds preds ctypes_sorts
   29.49    handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities")
   29.50  
   29.51  (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   29.52  fun preds_of_clauses clauses clsrel_clauses arity_clauses =
   29.53      Symtab.dest
   29.54 -        (foldl RC.add_classrelClause_preds
   29.55 -               (foldl RC.add_arityClause_preds
   29.56 -                      (foldl add_clause_preds Symtab.empty clauses)
   29.57 +        (List.foldl RC.add_classrelClause_preds
   29.58 +               (List.foldl RC.add_arityClause_preds
   29.59 +                      (List.foldl add_clause_preds Symtab.empty clauses)
   29.60                        arity_clauses)
   29.61                 clsrel_clauses)
   29.62  
   29.63 @@ -390,10 +390,10 @@
   29.64  
   29.65  fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
   29.66  
   29.67 -fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals;
   29.68 +fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
   29.69  
   29.70  fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
   29.71 -  if axiom_name mem_string user_lemmas then foldl count_literal ct literals
   29.72 +  if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
   29.73    else ct;
   29.74  
   29.75  fun cnf_helper_thms thy =
   29.76 @@ -402,8 +402,8 @@
   29.77  fun get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) =
   29.78    if isFO then []  (*first-order*)
   29.79    else
   29.80 -    let val ct0 = foldl count_clause init_counters conjectures
   29.81 -        val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
   29.82 +    let val ct0 = List.foldl count_clause init_counters conjectures
   29.83 +        val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
   29.84          fun needed c = valOf (Symtab.lookup ct c) > 0
   29.85          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
   29.86                   then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
   29.87 @@ -468,7 +468,7 @@
   29.88          val helper_clauses = get_helper_clauses false thy isFO (conjectures, axclauses, user_lemmas)
   29.89          val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses);
   29.90          val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_min_arity const_needs_hBOOL) conjectures)
   29.91 -        val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   29.92 +        val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
   29.93          val out = TextIO.openOut filename
   29.94      in
   29.95          List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) axclauses;
    30.1 --- a/src/HOL/Tools/res_reconstruct.ML	Sun Mar 01 16:48:06 2009 +0100
    30.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Sun Mar 01 23:36:12 2009 +0100
    30.3 @@ -51,7 +51,7 @@
    30.4  fun atom x = Br(x,[]);
    30.5  
    30.6  fun scons (x,y) = Br("cons", [x,y]);
    30.7 -val listof = foldl scons (atom "nil");
    30.8 +val listof = List.foldl scons (atom "nil");
    30.9  
   30.10  (*Strings enclosed in single quotes, e.g. filenames*)
   30.11  val quoted = $$"'" |-- Scan.repeat (~$$"'") --| $$"'" >> implode;
   30.12 @@ -243,7 +243,7 @@
   30.13  fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
   30.14  
   30.15  fun ints_of_stree_aux (Int n, ns) = n::ns
   30.16 -  | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts;
   30.17 +  | ints_of_stree_aux (Br(_,ts), ns) = List.foldl ints_of_stree_aux ns ts;
   30.18  
   30.19  fun ints_of_stree t = ints_of_stree_aux (t, []);
   30.20  
   30.21 @@ -362,7 +362,7 @@
   30.22  fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
   30.23  
   30.24  fun replace_deps (old:int, new) (lno, t, deps) =
   30.25 -      (lno, t, foldl (op union_int) [] (map (replace_dep (old, new)) deps));
   30.26 +      (lno, t, List.foldl (op union_int) [] (map (replace_dep (old, new)) deps));
   30.27  
   30.28  (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   30.29    only in type information.*)
   30.30 @@ -392,7 +392,7 @@
   30.31       then delete_dep lno lines
   30.32       else (lno, t, []) :: lines
   30.33    | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
   30.34 -and delete_dep lno lines = foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
   30.35 +and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
   30.36  
   30.37  fun bad_free (Free (a,_)) = String.isPrefix "sko_" a
   30.38    | bad_free _ = false;
   30.39 @@ -435,11 +435,11 @@
   30.40        val tuples = map (dest_tstp o tstp_line o explode) cnfs
   30.41        val _ = trace (Int.toString (length tuples) ^ " tuples extracted\n")
   30.42        val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
   30.43 -      val raw_lines = foldr add_prfline [] (decode_tstp_list ctxt tuples)
   30.44 +      val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
   30.45        val _ = trace (Int.toString (length raw_lines) ^ " raw_lines extracted\n")
   30.46 -      val nonnull_lines = foldr add_nonnull_prfline [] raw_lines
   30.47 +      val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
   30.48        val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
   30.49 -      val (_,lines) = foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
   30.50 +      val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
   30.51        val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
   30.52        val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
   30.53        val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
    31.1 --- a/src/HOL/Tools/simpdata.ML	Sun Mar 01 16:48:06 2009 +0100
    31.2 +++ b/src/HOL/Tools/simpdata.ML	Sun Mar 01 23:36:12 2009 +0100
    31.3 @@ -1,5 +1,4 @@
    31.4  (*  Title:      HOL/simpdata.ML
    31.5 -    ID:         $Id$
    31.6      Author:     Tobias Nipkow
    31.7      Copyright   1991  University of Cambridge
    31.8  
    31.9 @@ -65,7 +64,7 @@
   31.10      else
   31.11        let
   31.12          val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
   31.13 -        fun mk_simp_implies Q = foldr (fn (R, S) =>
   31.14 +        fun mk_simp_implies Q = List.foldr (fn (R, S) =>
   31.15            Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
   31.16          val aT = TFree ("'a", HOLogic.typeS);
   31.17          val x = Free ("x", aT);
    32.1 --- a/src/HOL/Tools/specification_package.ML	Sun Mar 01 16:48:06 2009 +0100
    32.2 +++ b/src/HOL/Tools/specification_package.ML	Sun Mar 01 23:36:12 2009 +0100
    32.3 @@ -120,7 +120,7 @@
    32.4                  val frees = OldTerm.term_frees prop
    32.5                  val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
    32.6                    orelse error "Specificaton: Only free variables of sort 'type' allowed"
    32.7 -                val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
    32.8 +                val prop_closed = List.foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
    32.9              in
   32.10                  (prop_closed,frees)
   32.11              end
   32.12 @@ -161,7 +161,7 @@
   32.13              in
   32.14                  HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop))
   32.15              end
   32.16 -        val ex_prop = foldr mk_exist prop proc_consts
   32.17 +        val ex_prop = List.foldr mk_exist prop proc_consts
   32.18          val cnames = map (fst o dest_Const) proc_consts
   32.19          fun post_process (arg as (thy,thm)) =
   32.20              let
    33.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Mar 01 16:48:06 2009 +0100
    33.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Mar 01 23:36:12 2009 +0100
    33.3 @@ -1,5 +1,4 @@
    33.4  (*  Title:      HOLCF/Tools/domain/domain_axioms.ML
    33.5 -    ID:         $Id$
    33.6      Author:     David von Oheimb
    33.7  
    33.8  Syntax generator for domain command.
    33.9 @@ -29,7 +28,7 @@
   33.10    val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
   33.11  
   33.12    val when_def = ("when_def",%%:(dname^"_when") == 
   33.13 -     foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
   33.14 +     List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
   33.15  				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
   33.16    
   33.17    val copy_def = let
   33.18 @@ -37,7 +36,7 @@
   33.19  			 then (cproj (Bound z) eqs (rec_of arg))`Bound(z-x)
   33.20  			 else Bound(z-x);
   33.21      fun one_con (con,args) =
   33.22 -        foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args;
   33.23 +        List.foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args;
   33.24    in ("copy_def", %%:(dname^"_copy") ==
   33.25         /\ "f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end;
   33.26  
   33.27 @@ -49,7 +48,7 @@
   33.28      fun inj y 1 _ = y
   33.29      |   inj y _ 0 = mk_sinl y
   33.30      |   inj y i j = mk_sinr (inj y (i-1) (j-1));
   33.31 -  in foldr /\# (dc_abs`(inj (parms args) m n)) args end;
   33.32 +  in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
   33.33    
   33.34    val con_defs = mapn (fn n => fn (con,args) =>
   33.35      (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
   33.36 @@ -57,14 +56,14 @@
   33.37    val dis_defs = let
   33.38  	fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
   33.39  		 list_ccomb(%%:(dname^"_when"),map 
   33.40 -			(fn (con',args) => (foldr /\#
   33.41 +			(fn (con',args) => (List.foldr /\#
   33.42  			   (if con'=con then TT else FF) args)) cons))
   33.43  	in map ddef cons end;
   33.44  
   33.45    val mat_defs = let
   33.46  	fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == 
   33.47  		 list_ccomb(%%:(dname^"_when"),map 
   33.48 -			(fn (con',args) => (foldr /\#
   33.49 +			(fn (con',args) => (List.foldr /\#
   33.50  			   (if con'=con
   33.51                                 then mk_return (mk_ctuple (map (bound_arg args) args))
   33.52                                 else mk_fail) args)) cons))
   33.53 @@ -79,7 +78,7 @@
   33.54            val r = Bound (length args);
   33.55            val rhs = case args of [] => mk_return HOLogic.unit
   33.56                                  | _ => mk_ctuple_pat ps ` mk_ctuple xs;
   33.57 -          fun one_con (con',args') = foldr /\# (if con'=con then rhs else mk_fail) args';
   33.58 +          fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
   33.59          in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
   33.60                 list_ccomb(%%:(dname^"_when"), map one_con cons))
   33.61          end
   33.62 @@ -89,7 +88,7 @@
   33.63  	fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
   33.64  		 list_ccomb(%%:(dname^"_when"),map 
   33.65  			(fn (con',args) => if con'<>con then UU else
   33.66 -			 foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
   33.67 +			 List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
   33.68  	in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
   33.69  
   33.70  
   33.71 @@ -152,11 +151,11 @@
   33.72  					 (allargs~~((allargs_cnt-1) downto 0)));
   33.73  	fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
   33.74  			   Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
   33.75 -	val capps = foldr mk_conj (mk_conj(
   33.76 +	val capps = List.foldr mk_conj (mk_conj(
   33.77  	   Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1),
   33.78  	   Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2)))
   33.79             (mapn rel_app 1 rec_args);
   33.80 -        in foldr mk_ex (Library.foldr mk_conj 
   33.81 +        in List.foldr mk_ex (Library.foldr mk_conj 
   33.82  			      (map (defined o Bound) nonlazy_idxs,capps)) allvns end;
   33.83        fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
   33.84  	 		proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
    34.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Sun Mar 01 16:48:06 2009 +0100
    34.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Sun Mar 01 23:36:12 2009 +0100
    34.3 @@ -1,5 +1,4 @@
    34.4  (*  Title:      HOLCF/Tools/domain/domain_library.ML
    34.5 -    ID:         $Id$
    34.6      Author:     David von Oheimb
    34.7  
    34.8  Library for domain command.
    34.9 @@ -15,7 +14,7 @@
   34.10  			     | itr [a] = f2 a
   34.11  			     | itr (a::l) = f(a, itr l)
   34.12  in  itr l  end;
   34.13 -fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
   34.14 +fun map_cumulr f start xs = List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
   34.15  						  (y::ys,res2)) ([],start) xs;
   34.16  
   34.17  
    35.1 --- a/src/HOLCF/Tools/domain/domain_syntax.ML	Sun Mar 01 16:48:06 2009 +0100
    35.2 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Sun Mar 01 23:36:12 2009 +0100
    35.3 @@ -1,5 +1,4 @@
    35.4  (*  Title:      HOLCF/Tools/domain/domain_syntax.ML
    35.5 -    ID:         $Id$
    35.6      Author:     David von Oheimb
    35.7  
    35.8  Syntax generator for domain command.
    35.9 @@ -22,14 +21,14 @@
   35.10  			    else foldr1 mk_sprodT (map opt_lazy args);
   35.11    fun freetvar s = let val tvar = mk_TFree s in
   35.12  		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
   35.13 -  fun when_type (_   ,_,args) = foldr (op ->>) (freetvar "t") (map third args);
   35.14 +  fun when_type (_   ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args);
   35.15  in
   35.16    val dtype  = Type(dname,typevars);
   35.17    val dtype2 = foldr1 mk_ssumT (map prod cons');
   35.18    val dnam = Sign.base_name dname;
   35.19    val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
   35.20    val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
   35.21 -  val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
   35.22 +  val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
   35.23    val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
   35.24  end;
   35.25  
   35.26 @@ -41,7 +40,7 @@
   35.27  							 else      c::esc cs
   35.28  	|   esc []      = []
   35.29  	in implode o esc o Symbol.explode end;
   35.30 -  fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s);
   35.31 +  fun con (name,s,args) = (name, List.foldr (op ->>) dtype (map third args),s);
   35.32    fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
   35.33  			   Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
   35.34  			(* strictly speaking, these constants have one argument,
   35.35 @@ -86,7 +85,7 @@
   35.36      val capp = app "Rep_CFun";
   35.37      fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args);
   35.38      fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n);
   35.39 -    fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
   35.40 +    fun arg1 n (con,_,args) = List.foldr cabs (expvar n) (argvars n args);
   35.41      fun when1 n m = if n = m then arg1 n else K (Constant "UU");
   35.42  
   35.43      fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
    36.1 --- a/src/Provers/blast.ML	Sun Mar 01 16:48:06 2009 +0100
    36.2 +++ b/src/Provers/blast.ML	Sun Mar 01 23:36:12 2009 +0100
    36.3 @@ -1,5 +1,4 @@
    36.4  (*  Title:      Provers/blast.ML
    36.5 -    ID:         $Id$
    36.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    36.7      Copyright   1997  University of Cambridge
    36.8  
    36.9 @@ -764,8 +763,8 @@
   36.10              end
   36.11        (*substitute throughout "stack frame"; extract affected formulae*)
   36.12        fun subFrame ((Gs,Hs), (changed, frames)) =
   36.13 -            let val (changed', Gs') = foldr subForm (changed, []) Gs
   36.14 -                val (changed'', Hs') = foldr subForm (changed', []) Hs
   36.15 +            let val (changed', Gs') = List.foldr subForm (changed, []) Gs
   36.16 +                val (changed'', Hs') = List.foldr subForm (changed', []) Hs
   36.17              in  (changed'', (Gs',Hs')::frames)  end
   36.18        (*substitute throughout literals; extract affected ones*)
   36.19        fun subLit (lit, (changed, nlits)) =
   36.20 @@ -773,8 +772,8 @@
   36.21              in  if nlit aconv lit then (changed, nlit::nlits)
   36.22                                    else ((nlit,true)::changed, nlits)
   36.23              end
   36.24 -      val (changed, lits') = foldr subLit ([], []) lits
   36.25 -      val (changed', pairs') = foldr subFrame (changed, []) pairs
   36.26 +      val (changed, lits') = List.foldr subLit ([], []) lits
   36.27 +      val (changed', pairs') = List.foldr subFrame (changed, []) pairs
   36.28    in  if !trace then writeln ("Substituting " ^ traceTerm thy u ^
   36.29                                " for " ^ traceTerm thy t ^ " in branch" )
   36.30        else ();
   36.31 @@ -971,7 +970,7 @@
   36.32                                      then lim - (1+log(length rules))
   36.33                                      else lim   (*discourage branching updates*)
   36.34                           val vars  = vars_in_vars vars
   36.35 -                         val vars' = foldr add_terms_vars vars prems
   36.36 +                         val vars' = List.foldr add_terms_vars vars prems
   36.37                           val choices' = (ntrl, nbrs, PRV) :: choices
   36.38                           val tacs' = (tac(updated,false,true))
   36.39                                       :: tacs  (*no duplication; rotate*)
   36.40 @@ -1098,7 +1097,7 @@
   36.41                      then
   36.42                       let val updated = ntrl < !ntrail (*branch updated*)
   36.43                           val vars  = vars_in_vars vars
   36.44 -                         val vars' = foldr add_terms_vars vars prems
   36.45 +                         val vars' = List.foldr add_terms_vars vars prems
   36.46                              (*duplicate H if md permits*)
   36.47                           val dup = md (*earlier had "andalso vars' <> vars":
   36.48                                    duplicate only if the subgoal has new vars*)
    37.1 --- a/src/Provers/clasimp.ML	Sun Mar 01 16:48:06 2009 +0100
    37.2 +++ b/src/Provers/clasimp.ML	Sun Mar 01 23:36:12 2009 +0100
    37.3 @@ -1,5 +1,4 @@
    37.4  (*  Title:      Provers/clasimp.ML
    37.5 -    ID:         $Id$
    37.6      Author:     David von Oheimb, TU Muenchen
    37.7  
    37.8  Combination of classical reasoner and simplifier (depends on
    37.9 @@ -153,7 +152,7 @@
   37.10    end;
   37.11  
   37.12  fun modifier att (x, ths) =
   37.13 -  fst (foldl_map (Library.apply [att]) (x, rev ths));
   37.14 +  fst (Library.foldl_map (Library.apply [att]) (x, rev ths));
   37.15  
   37.16  val addXIs = modifier (ContextRules.intro_query NONE);
   37.17  val addXEs = modifier (ContextRules.elim_query NONE);
    38.1 --- a/src/Provers/classical.ML	Sun Mar 01 16:48:06 2009 +0100
    38.2 +++ b/src/Provers/classical.ML	Sun Mar 01 23:36:12 2009 +0100
    38.3 @@ -223,7 +223,7 @@
    38.4      let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
    38.5      in  assume_tac      ORELSE'
    38.6          contr_tac       ORELSE'
    38.7 -        biresolve_tac (foldr addrl [] rls)
    38.8 +        biresolve_tac (List.foldr addrl [] rls)
    38.9      end;
   38.10  
   38.11  (*Duplication of hazardous rules, for complete provers*)
    39.1 --- a/src/Provers/order.ML	Sun Mar 01 16:48:06 2009 +0100
    39.2 +++ b/src/Provers/order.ML	Sun Mar 01 23:36:12 2009 +0100
    39.3 @@ -639,7 +639,7 @@
    39.4  
    39.5     (* Compute, for each adjacency list, the list with reversed edges,
    39.6        and concatenate these lists. *)
    39.7 -   val flipped = foldr (op @) nil (map flip g)
    39.8 +   val flipped = List.foldr (op @) nil (map flip g)
    39.9   
   39.10   in assemble g flipped end    
   39.11        
   39.12 @@ -677,7 +677,7 @@
   39.13        let
   39.14     val _ = visited := u :: !visited
   39.15     val descendents =
   39.16 -       foldr (fn ((v,l),ds) => if been_visited v then ds
   39.17 +       List.foldr (fn ((v,l),ds) => if been_visited v then ds
   39.18              else v :: dfs_visit g v @ ds)
   39.19          nil (adjacent (op aconv) g u)
   39.20        in
   39.21 @@ -727,7 +727,7 @@
   39.22        let
   39.23     val _ = visited := u :: !visited
   39.24     val descendents =
   39.25 -       foldr (fn ((v,l),ds) => if been_visited v then ds
   39.26 +       List.foldr (fn ((v,l),ds) => if been_visited v then ds
   39.27              else v :: dfs_visit g v @ ds)
   39.28          nil (adjacent (op =) g u)
   39.29     in  descendents end
    40.1 --- a/src/Provers/trancl.ML	Sun Mar 01 16:48:06 2009 +0100
    40.2 +++ b/src/Provers/trancl.ML	Sun Mar 01 23:36:12 2009 +0100
    40.3 @@ -1,8 +1,6 @@
    40.4  (*
    40.5 -  Title:	Transitivity reasoner for transitive closures of relations
    40.6 -  Id:		$Id$
    40.7 -  Author:	Oliver Kutter
    40.8 -  Copyright:	TU Muenchen
    40.9 +    Title:      Transitivity reasoner for transitive closures of relations
   40.10 +    Author:     Oliver Kutter, TU Muenchen
   40.11  *)
   40.12  
   40.13  (*
   40.14 @@ -335,7 +333,7 @@
   40.15  
   40.16     (* Compute, for each adjacency list, the list with reversed edges,
   40.17        and concatenate these lists. *)
   40.18 -   val flipped = foldr (op @) nil (map flip g)
   40.19 +   val flipped = List.foldr (op @) nil (map flip g)
   40.20   
   40.21   in assemble g flipped end    
   40.22   
   40.23 @@ -359,7 +357,7 @@
   40.24        let
   40.25     val _ = visited := u :: !visited
   40.26     val descendents =
   40.27 -       foldr (fn ((v,l),ds) => if been_visited v then ds
   40.28 +       List.foldr (fn ((v,l),ds) => if been_visited v then ds
   40.29              else v :: dfs_visit g v @ ds)
   40.30          nil (adjacent eq_comp g u)
   40.31     in  descendents end
    41.1 --- a/src/Provers/typedsimp.ML	Sun Mar 01 16:48:06 2009 +0100
    41.2 +++ b/src/Provers/typedsimp.ML	Sun Mar 01 23:36:12 2009 +0100
    41.3 @@ -1,5 +1,4 @@
    41.4  (*  Title: 	typedsimp
    41.5 -    ID:         $Id$
    41.6      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    41.7      Copyright   1993  University of Cambridge
    41.8  
    41.9 @@ -70,7 +69,7 @@
   41.10      handle THM _ => (simp_rls, rl :: other_rls);
   41.11  
   41.12  (*Given the list rls, return the pair (simp_rls, other_rls).*)
   41.13 -fun process_rules rls = foldr add_rule ([],[]) rls;
   41.14 +fun process_rules rls = List.foldr add_rule ([],[]) rls;
   41.15  
   41.16  (*Given list of rewrite rules, return list of both forms, reject others*)
   41.17  fun process_rewrites rls = 
    42.1 --- a/src/Pure/Isar/attrib.ML	Sun Mar 01 16:48:06 2009 +0100
    42.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 01 23:36:12 2009 +0100
    42.3 @@ -198,7 +198,7 @@
    42.4        let
    42.5          val ths = Facts.select thmref fact;
    42.6          val atts = map (attribute_i thy) srcs;
    42.7 -        val (context', ths') = foldl_map (Library.apply atts) (context, ths);
    42.8 +        val (context', ths') = Library.foldl_map (Library.apply atts) (context, ths);
    42.9        in (context', pick name ths') end)
   42.10    end);
   42.11  
    43.1 --- a/src/Pure/Isar/method.ML	Sun Mar 01 16:48:06 2009 +0100
    43.2 +++ b/src/Pure/Isar/method.ML	Sun Mar 01 23:36:12 2009 +0100
    43.3 @@ -436,7 +436,7 @@
    43.4  local
    43.5  
    43.6  fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
    43.7 -fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
    43.8 +fun app (f, att) (context, ths) = Library.foldl_map att (Context.map_proof f context, ths);
    43.9  
   43.10  fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
   43.11    (fn (m, ths) => Scan.succeed (app m (context, ths))));
    44.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 01 16:48:06 2009 +0100
    44.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Mar 01 23:36:12 2009 +0100
    44.3 @@ -975,7 +975,7 @@
    44.4  
    44.5      val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
    44.6      fun app (th, attrs) x =
    44.7 -      swap (foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
    44.8 +      swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
    44.9      val (res, ctxt') = fold_map app facts ctxt;
   44.10      val thms = PureThy.name_thms false false pos name (flat res);
   44.11      val Mode {stmt, ...} = get_mode ctxt;
    45.1 --- a/src/Pure/Proof/reconstruct.ML	Sun Mar 01 16:48:06 2009 +0100
    45.2 +++ b/src/Pure/Proof/reconstruct.ML	Sun Mar 01 23:36:12 2009 +0100
    45.3 @@ -106,7 +106,7 @@
    45.4  
    45.5  fun decompose thy Ts (env, p as (t, u)) =
    45.6    let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p
    45.7 -    else apsnd flat (foldl_map (decompose thy Ts) (uT env T U, ts ~~ us))
    45.8 +    else apsnd flat (Library.foldl_map (decompose thy Ts) (uT env T U, ts ~~ us))
    45.9    in case pairself (strip_comb o Envir.head_norm env) p of
   45.10        ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us
   45.11      | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us
   45.12 @@ -141,7 +141,7 @@
   45.13              val tvars = OldTerm.term_tvars prop;
   45.14              val tfrees = OldTerm.term_tfrees prop;
   45.15              val (env', Ts) = (case opTs of
   45.16 -                NONE => foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
   45.17 +                NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
   45.18                | SOME Ts => (env, Ts));
   45.19              val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
   45.20                (forall_intr_vfs prop) handle Library.UnequalLengths =>
    46.1 --- a/src/Pure/Tools/find_consts.ML	Sun Mar 01 16:48:06 2009 +0100
    46.2 +++ b/src/Pure/Tools/find_consts.ML	Sun Mar 01 23:36:12 2009 +0100
    46.3 @@ -111,7 +111,7 @@
    46.4      val criteria = map make_criterion (! default_criteria @ raw_criteria);
    46.5  
    46.6      val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy;
    46.7 -    fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria;
    46.8 +    fun eval_entry c = List.foldl filter_const (SOME (c, low_ranking)) criteria;
    46.9  
   46.10      val matches =
   46.11        Symtab.fold (cons o eval_entry) consts []
    47.1 --- a/src/Pure/library.ML	Sun Mar 01 16:48:06 2009 +0100
    47.2 +++ b/src/Pure/library.ML	Sun Mar 01 23:36:12 2009 +0100
    47.3 @@ -76,7 +76,6 @@
    47.4    val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
    47.5    val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a
    47.6    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    47.7 -  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    47.8    val flat: 'a list list -> 'a list
    47.9    val unflat: 'a list list -> 'b list -> 'b list list
   47.10    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
   47.11 @@ -238,6 +237,7 @@
   47.12    include BASIC_LIBRARY
   47.13    val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   47.14    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   47.15 +  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   47.16    val take: int * 'a list -> 'a list
   47.17    val drop: int * 'a list -> 'a list
   47.18    val last_elem: 'a list -> 'a
    48.1 --- a/src/Pure/pure_thy.ML	Sun Mar 01 16:48:06 2009 +0100
    48.2 +++ b/src/Pure/pure_thy.ML	Sun Mar 01 23:36:12 2009 +0100
    48.3 @@ -177,7 +177,7 @@
    48.4  
    48.5  fun add_thms_atts pre_name ((b, thms), atts) =
    48.6    enter_thms pre_name (name_thms false true Position.none)
    48.7 -    (foldl_map (Thm.theory_attributes atts)) (b, thms);
    48.8 +    (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
    48.9  
   48.10  fun gen_add_thmss pre_name =
   48.11    fold_map (add_thms_atts pre_name);
   48.12 @@ -207,9 +207,9 @@
   48.13      val name = Sign.full_name thy b;
   48.14      val _ = Position.report (Markup.fact_decl name) pos;
   48.15  
   48.16 -    fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
   48.17 +    fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
   48.18      val (thms, thy') = thy |> enter_thms
   48.19 -      (name_thmss true pos) (name_thms false true pos) (apsnd flat o foldl_map app)
   48.20 +      (name_thmss true pos) (name_thms false true pos) (apsnd flat o Library.foldl_map app)
   48.21        (b, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
   48.22    in ((name, thms), thy') end);
   48.23  
    49.1 --- a/src/Tools/IsaPlanner/isand.ML	Sun Mar 01 16:48:06 2009 +0100
    49.2 +++ b/src/Tools/IsaPlanner/isand.ML	Sun Mar 01 23:36:12 2009 +0100
    49.3 @@ -132,7 +132,7 @@
    49.4        fun allify_prem_var (vt as (n,ty),t)  = 
    49.5            (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    49.6  
    49.7 -      fun allify_prem Ts p = foldr allify_prem_var p Ts
    49.8 +      fun allify_prem Ts p = List.foldr allify_prem_var p Ts
    49.9  
   49.10        val cTs = map (ctermify o Free) Ts
   49.11        val cterm_asms = map (ctermify o allify_prem Ts) premts
   49.12 @@ -306,7 +306,7 @@
   49.13      in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
   49.14  
   49.15  fun allify_for_sg_term ctermify vs t =
   49.16 -    let val t_alls = foldr allify_term t vs;
   49.17 +    let val t_alls = List.foldr allify_term t vs;
   49.18          val ct_alls = ctermify t_alls; 
   49.19      in 
   49.20        (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
   49.21 @@ -394,7 +394,7 @@
   49.22                  |> Drule.forall_intr_list cfvs
   49.23      in Drule.compose_single (solth', i, gth) end;
   49.24  
   49.25 -fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
   49.26 +fun export_solutions (xs,th) = List.foldr (uncurry export_solution) th xs;
   49.27  
   49.28  
   49.29  (* fix parameters of a subgoal "i", as free variables, and create an
    50.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Sun Mar 01 16:48:06 2009 +0100
    50.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Sun Mar 01 23:36:12 2009 +0100
    50.3 @@ -136,7 +136,7 @@
    50.4  fun mk_renamings tgt rule_inst = 
    50.5      let
    50.6        val rule_conds = Thm.prems_of rule_inst
    50.7 -      val names = foldr OldTerm.add_term_names [] (tgt :: rule_conds);
    50.8 +      val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
    50.9        val (conds_tyvs,cond_vs) = 
   50.10            Library.foldl (fn ((tyvs, vs), t) => 
   50.11                      (Library.union
   50.12 @@ -147,7 +147,7 @@
   50.13        val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
   50.14        val vars_to_fix = Library.union (termvars, cond_vs);
   50.15        val (renamings, names2) = 
   50.16 -          foldr (fn (((n,i),ty), (vs, names')) => 
   50.17 +          List.foldr (fn (((n,i),ty), (vs, names')) => 
   50.18                      let val n' = Name.variant names' n in
   50.19                        ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
   50.20                      end)
   50.21 @@ -166,13 +166,13 @@
   50.22      let 
   50.23        val ignore_ixs = map fst ignore_insts;
   50.24        val (tvars, tfrees) = 
   50.25 -            foldr (fn (t, (varixs, tfrees)) => 
   50.26 +            List.foldr (fn (t, (varixs, tfrees)) => 
   50.27                        (OldTerm.add_term_tvars (t,varixs),
   50.28                         OldTerm.add_term_tfrees (t,tfrees)))
   50.29                    ([],[]) ts;
   50.30          val unfixed_tvars = 
   50.31              List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
   50.32 -        val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
   50.33 +        val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
   50.34      in (fixtyinsts, tfrees) end;
   50.35  
   50.36  
   50.37 @@ -248,7 +248,7 @@
   50.38                            Ts;
   50.39  
   50.40        (* type-instantiate the var instantiations *)
   50.41 -      val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => 
   50.42 +      val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) => 
   50.43                              (ix, (Term.typ_subst_TVars term_typ_inst ty, 
   50.44                                    Term.subst_TVars term_typ_inst t))
   50.45                              :: insts_tyinst)
    51.1 --- a/src/ZF/Tools/datatype_package.ML	Sun Mar 01 16:48:06 2009 +0100
    51.2 +++ b/src/ZF/Tools/datatype_package.ML	Sun Mar 01 23:36:12 2009 +0100
    51.3 @@ -1,5 +1,4 @@
    51.4  (*  Title:      ZF/Tools/datatype_package.ML
    51.5 -    ID:         $Id$
    51.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    51.7      Copyright   1994  University of Cambridge
    51.8  
    51.9 @@ -140,11 +139,11 @@
   51.10    (*Treatment of a list of constructors, for one part
   51.11      Result adds a list of terms, each a function variable with arguments*)
   51.12    fun add_case_list (con_ty_list, (opno, case_lists)) =
   51.13 -    let val (opno', case_list) = foldr add_case (opno, []) con_ty_list
   51.14 +    let val (opno', case_list) = List.foldr add_case (opno, []) con_ty_list
   51.15      in (opno', case_list :: case_lists) end;
   51.16  
   51.17    (*Treatment of all parts*)
   51.18 -  val (_, case_lists) = foldr add_case_list (1,[]) con_ty_lists;
   51.19 +  val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists;
   51.20  
   51.21    (*extract the types of all the variables*)
   51.22    val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"};
   51.23 @@ -184,7 +183,7 @@
   51.24            val rec_args = map (make_rec_call (rev case_args,0))
   51.25                           (List.drop(recursor_args, ncase_args))
   51.26        in
   51.27 -          foldr add_abs
   51.28 +          List.foldr add_abs
   51.29              (list_comb (recursor_var,
   51.30                          bound_args @ rec_args)) case_args
   51.31        end
   51.32 @@ -216,7 +215,7 @@
   51.33    val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
   51.34  
   51.35    (*Treatment of all parts*)
   51.36 -  val (_, recursor_lists) = foldr add_case_list (1,[]) rec_ty_lists;
   51.37 +  val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists;
   51.38  
   51.39    (*extract the types of all the variables*)
   51.40    val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"};
    52.1 --- a/src/ZF/Tools/inductive_package.ML	Sun Mar 01 16:48:06 2009 +0100
    52.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun Mar 01 23:36:12 2009 +0100
    52.3 @@ -99,7 +99,7 @@
    52.4                 Syntax.string_of_term ctxt t);
    52.5  
    52.6    (*** Construct the fixedpoint definition ***)
    52.7 -  val mk_variant = Name.variant (foldr OldTerm.add_term_names [] intr_tms);
    52.8 +  val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
    52.9  
   52.10    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
   52.11  
   52.12 @@ -113,7 +113,7 @@
   52.13          val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
   52.14          val exfrees = OldTerm.term_frees intr \\ rec_params
   52.15          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
   52.16 -    in foldr FOLogic.mk_exists
   52.17 +    in List.foldr FOLogic.mk_exists
   52.18               (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees
   52.19      end;
   52.20  
   52.21 @@ -303,7 +303,7 @@
   52.22       (*Make a premise of the induction rule.*)
   52.23       fun induct_prem ind_alist intr =
   52.24         let val quantfrees = map dest_Free (OldTerm.term_frees intr \\ rec_params)
   52.25 -           val iprems = foldr (add_induct_prem ind_alist) []
   52.26 +           val iprems = List.foldr (add_induct_prem ind_alist) []
   52.27                                (Logic.strip_imp_prems intr)
   52.28             val (t,X) = Ind_Syntax.rule_concl intr
   52.29             val (SOME pred) = AList.lookup (op aconv) ind_alist X
   52.30 @@ -380,7 +380,7 @@
   52.31             val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
   52.32                              elem_factors ---> FOLogic.oT)
   52.33             val qconcl =
   52.34 -             foldr FOLogic.mk_all
   52.35 +             List.foldr FOLogic.mk_all
   52.36                 (FOLogic.imp $
   52.37                  (@{const mem} $ elem_tuple $ rec_tm)
   52.38                        $ (list_comb (pfree, elem_frees))) elem_frees
    53.1 --- a/src/ZF/Tools/primrec_package.ML	Sun Mar 01 16:48:06 2009 +0100
    53.2 +++ b/src/ZF/Tools/primrec_package.ML	Sun Mar 01 23:36:12 2009 +0100
    53.3 @@ -120,7 +120,7 @@
    53.4                | SOME (rhs, cargs', eq) =>
    53.5                      (rhs, inst_recursor (recursor_pair, cargs'), eq)
    53.6            val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
    53.7 -          val abs = foldr absterm rhs allowed_terms
    53.8 +          val abs = List.foldr absterm rhs allowed_terms
    53.9        in
   53.10            if !Ind_Syntax.trace then
   53.11                writeln ("recursor_rhs = " ^
   53.12 @@ -145,7 +145,7 @@
   53.13      val def_tm = Logic.mk_equals
   53.14                      (subst_bound (rec_arg, fabs),
   53.15                       list_comb (recursor,
   53.16 -                                foldr add_case [] (cnames ~~ recursor_pairs))
   53.17 +                                List.foldr add_case [] (cnames ~~ recursor_pairs))
   53.18                       $ rec_arg)
   53.19  
   53.20    in
   53.21 @@ -164,7 +164,7 @@
   53.22    let
   53.23      val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args);
   53.24      val SOME (fname, ftype, ls, rs, con_info, eqns) =
   53.25 -      foldr (process_eqn thy) NONE eqn_terms;
   53.26 +      List.foldr (process_eqn thy) NONE eqn_terms;
   53.27      val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
   53.28  
   53.29      val ([def_thm], thy1) = thy