merged
authorwenzelm
Thu Oct 29 23:58:15 2009 +0100 (2009-10-29)
changeset 333476748bd742d7a
parent 33346 c5cd93763e71
parent 33339 d41f77196338
child 33348 bb65583ab70d
merged
     1.1 --- a/src/FOLP/simp.ML	Thu Oct 29 23:17:35 2009 +0100
     1.2 +++ b/src/FOLP/simp.ML	Thu Oct 29 23:58:15 2009 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4  fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2);
     1.5  
     1.6  (*insert a thm in a discrimination net by its lhs*)
     1.7 -fun lhs_insert_thm (th,net) =
     1.8 +fun lhs_insert_thm th net =
     1.9      Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net
    1.10      handle  Net.INSERT => net;
    1.11  
    1.12 @@ -434,7 +434,7 @@
    1.13          val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
    1.14          val new_rws = maps mk_rew_rules thms;
    1.15          val rwrls = map mk_trans (maps mk_rew_rules thms);
    1.16 -        val anet' = List.foldr lhs_insert_thm anet rwrls
    1.17 +        val anet' = fold_rev lhs_insert_thm rwrls anet;
    1.18      in  if !tracing andalso not(null new_rws)
    1.19          then writeln (cat_lines
    1.20            ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
     2.1 --- a/src/HOL/Import/lazy_seq.ML	Thu Oct 29 23:17:35 2009 +0100
     2.2 +++ b/src/HOL/Import/lazy_seq.ML	Thu Oct 29 23:58:15 2009 +0100
     2.3 @@ -407,8 +407,8 @@
     2.4          make (fn () => copy (f x))
     2.5      end
     2.6  
     2.7 -fun EVERY fs = List.foldr (op THEN) succeed fs
     2.8 -fun FIRST fs = List.foldr (op ORELSE) fail fs
     2.9 +fun EVERY fs = fold_rev (curry op THEN) fs succeed
    2.10 +fun FIRST fs = fold_rev (curry op ORELSE) fs fail
    2.11  
    2.12  fun TRY f x =
    2.13      make (fn () =>
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Oct 29 23:17:35 2009 +0100
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 29 23:58:15 2009 +0100
     3.3 @@ -776,7 +776,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 = List.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
     3.8 +                val tg = fold_rev (Tag.merge o Tag.read) ors Tag.empty_tag
     3.9              in
    3.10                  mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
    3.11              end
    3.12 @@ -1160,7 +1160,7 @@
    3.13          | replace_name n' _ = ERR "replace_name"
    3.14        (* map: old or fresh name -> old free,
    3.15           invmap: old free which has fresh name assigned to it -> fresh name *)
    3.16 -      fun dis (v, mapping as (map,invmap)) =
    3.17 +      fun dis v (mapping as (map,invmap)) =
    3.18            let val n = name_of v in
    3.19              case Symtab.lookup map n of
    3.20                NONE => (Symtab.update (n, v) map, invmap)
    3.21 @@ -1179,11 +1179,11 @@
    3.22        else
    3.23          let
    3.24            val (_, invmap) =
    3.25 -              List.foldl dis (Symtab.empty, Termtab.empty) frees
    3.26 -          fun make_subst ((oldfree, newname), (intros, elims)) =
    3.27 +              fold dis frees (Symtab.empty, Termtab.empty)
    3.28 +          fun make_subst (oldfree, newname) (intros, elims) =
    3.29                (cterm_of thy oldfree :: intros,
    3.30                 cterm_of thy (replace_name newname oldfree) :: elims)
    3.31 -          val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap)
    3.32 +          val (intros, elims) = fold make_subst (Termtab.dest invmap) ([], [])
    3.33          in
    3.34            forall_elim_list elims (forall_intr_list intros thm)
    3.35          end
    3.36 @@ -1837,7 +1837,7 @@
    3.37                        | inst_type ty1 ty2 (ty as Type(name,tys)) =
    3.38                          Type(name,map (inst_type ty1 ty2) tys)
    3.39                  in
    3.40 -                    List.foldr (fn (v,th) =>
    3.41 +                    fold_rev (fn v => fn th =>
    3.42                                let
    3.43                                    val cdom = fst (dom_rng (fst (dom_rng cty)))
    3.44                                    val vty  = type_of v
    3.45 @@ -1845,11 +1845,11 @@
    3.46                                    val cc = cterm_of thy (Const(cname,newcty))
    3.47                                in
    3.48                                    mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
    3.49 -                              end) th vlist'
    3.50 +                              end) vlist' th
    3.51                  end
    3.52                | SOME _ => raise ERR "GEN_ABS" "Bad constant"
    3.53                | NONE =>
    3.54 -                List.foldr (fn (v,th) => mk_ABS v th thy) th vlist'
    3.55 +                fold_rev (fn v => fn th => mk_ABS v th thy) vlist' th
    3.56          val res = HOLThm(rens_of info',th1)
    3.57          val _ = message "RESULT:"
    3.58          val _ = if_debug pth res
    3.59 @@ -2020,8 +2020,8 @@
    3.60                                 Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy'
    3.61                             end
    3.62  
    3.63 -            val thy1 = List.foldr (fn(name,thy)=>
    3.64 -                                snd (get_defname thyname name thy)) thy1 names
    3.65 +            val thy1 = fold_rev (fn name => fn thy =>
    3.66 +                                snd (get_defname thyname name thy)) names thy1
    3.67              fun new_name name = fst (get_defname thyname name thy1)
    3.68              val names' = map (fn name => (new_name name,name,false)) names
    3.69              val (thy',res) = Choice_Specification.add_specification NONE
    3.70 @@ -2041,12 +2041,12 @@
    3.71                       then quotename name
    3.72                       else (quotename newname) ^ ": " ^ (quotename name),thy')
    3.73                  end
    3.74 -            val (new_names,thy') = List.foldr (fn(name,(names,thy)) =>
    3.75 +            val (new_names,thy') = fold_rev (fn name => fn (names, thy) =>
    3.76                                              let
    3.77                                                  val (name',thy') = handle_const (name,thy)
    3.78                                              in
    3.79                                                  (name'::names,thy')
    3.80 -                                            end) ([],thy') names
    3.81 +                                            end) names ([], thy')
    3.82              val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
    3.83                                    "\n  by (import " ^ thyname ^ " " ^ thmname ^ ")")
    3.84                                   thy'
     4.1 --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Oct 29 23:17:35 2009 +0100
     4.2 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Oct 29 23:58:15 2009 +0100
     4.3 @@ -100,7 +100,7 @@
     4.4    (fn (x, k) => (cterm_of (ProofContext.theory_of ctxt) (Free (x, @{typ real})), k)) 
     4.5  
     4.6  fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
     4.7 -  List.foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.empty
     4.8 +  (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
     4.9  
    4.10  fun parse_cmonomial ctxt =
    4.11    rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
    4.12 @@ -108,7 +108,7 @@
    4.13    rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
    4.14  
    4.15  fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
    4.16 -  List.foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.empty
    4.17 +  (fn xs => fold FuncUtil.Monomialfunc.update xs FuncUtil.Monomialfunc.empty)
    4.18  
    4.19  (* positivstellensatz parser *)
    4.20  
     5.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 23:17:35 2009 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 23:58:15 2009 +0100
     5.3 @@ -526,7 +526,7 @@
     5.4  
     5.5      fun make_intr s T (cname, cargs) =
     5.6        let
     5.7 -        fun mk_prem (dt, (j, j', prems, ts)) =
     5.8 +        fun mk_prem dt (j, j', prems, ts) =
     5.9            let
    5.10              val (dts, dt') = strip_option dt;
    5.11              val (dts', dt'') = strip_dtyp dt';
    5.12 @@ -535,7 +535,7 @@
    5.13              val T = typ_of_dtyp descr sorts dt'';
    5.14              val free = mk_Free "x" (Us ---> T) j;
    5.15              val free' = app_bnds free (length Us);
    5.16 -            fun mk_abs_fun (T, (i, t)) =
    5.17 +            fun mk_abs_fun T (i, t) =
    5.18                let val U = fastype_of t
    5.19                in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
    5.20                  Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
    5.21 @@ -546,10 +546,10 @@
    5.22                    HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
    5.23                      T --> HOLogic.boolT) $ free')) :: prems
    5.24                | _ => prems,
    5.25 -            snd (List.foldr mk_abs_fun (j', free) Ts) :: ts)
    5.26 +            snd (fold_rev mk_abs_fun Ts (j', free)) :: ts)
    5.27            end;
    5.28  
    5.29 -        val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs;
    5.30 +        val (_, _, prems, ts) = fold_rev mk_prem cargs (1, 1, [], []);
    5.31          val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
    5.32            list_comb (Const (cname, map fastype_of ts ---> T), ts))
    5.33        in Logic.list_implies (prems, concl)
    5.34 @@ -710,7 +710,7 @@
    5.35  
    5.36      (**** constructors ****)
    5.37  
    5.38 -    fun mk_abs_fun (x, t) =
    5.39 +    fun mk_abs_fun x t =
    5.40        let
    5.41          val T = fastype_of x;
    5.42          val U = fastype_of t
    5.43 @@ -776,7 +776,7 @@
    5.44      fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx))
    5.45          (thy, defs, eqns) =
    5.46        let
    5.47 -        fun constr_arg ((dts, dt), (j, l_args, r_args)) =
    5.48 +        fun constr_arg (dts, dt) (j, l_args, r_args) =
    5.49            let
    5.50              val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
    5.51                (dts ~~ (j upto j + length dts - 1))
    5.52 @@ -784,16 +784,16 @@
    5.53            in
    5.54              (j + length dts + 1,
    5.55               xs @ x :: l_args,
    5.56 -             List.foldr mk_abs_fun
    5.57 +             fold_rev mk_abs_fun xs
    5.58                 (case dt of
    5.59                    DtRec k => if k < length new_type_names then
    5.60                        Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
    5.61                          typ_of_dtyp descr sorts dt) $ x
    5.62                      else error "nested recursion not (yet) supported"
    5.63 -                | _ => x) xs :: r_args)
    5.64 +                | _ => x) :: r_args)
    5.65            end
    5.66  
    5.67 -        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
    5.68 +        val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
    5.69          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
    5.70          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
    5.71          val constrT = map fastype_of l_args ---> T;
    5.72 @@ -902,7 +902,7 @@
    5.73              let val T = fastype_of t
    5.74              in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
    5.75  
    5.76 -          fun constr_arg ((dts, dt), (j, l_args, r_args)) =
    5.77 +          fun constr_arg (dts, dt) (j, l_args, r_args) =
    5.78              let
    5.79                val Ts = map (typ_of_dtyp descr'' sorts) dts;
    5.80                val xs = map (fn (T, i) => mk_Free "x" T i)
    5.81 @@ -914,7 +914,7 @@
    5.82                 map perm (xs @ [x]) @ r_args)
    5.83              end
    5.84  
    5.85 -          val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
    5.86 +          val (_, l_args, r_args) = fold_rev constr_arg dts (1, [], []);
    5.87            val c = Const (cname, map fastype_of l_args ---> T)
    5.88          in
    5.89            Goal.prove_global thy8 [] []
    5.90 @@ -952,7 +952,7 @@
    5.91            val cname = Sign.intern_const thy8
    5.92              (Long_Name.append tname (Long_Name.base_name cname));
    5.93  
    5.94 -          fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
    5.95 +          fun make_inj (dts, dt) (j, args1, args2, eqs) =
    5.96              let
    5.97                val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
    5.98                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
    5.99 @@ -963,10 +963,10 @@
   5.100                (j + length dts + 1,
   5.101                 xs @ (x :: args1), ys @ (y :: args2),
   5.102                 HOLogic.mk_eq
   5.103 -                 (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs)
   5.104 +                 (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs)
   5.105              end;
   5.106  
   5.107 -          val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts;
   5.108 +          val (_, args1, args2, eqs) = fold_rev make_inj dts (1, [], [], []);
   5.109            val Ts = map fastype_of args1;
   5.110            val c = Const (cname, Ts ---> T)
   5.111          in
   5.112 @@ -995,17 +995,17 @@
   5.113              (Long_Name.append tname (Long_Name.base_name cname));
   5.114            val atomT = Type (atom, []);
   5.115  
   5.116 -          fun process_constr ((dts, dt), (j, args1, args2)) =
   5.117 +          fun process_constr (dts, dt) (j, args1, args2) =
   5.118              let
   5.119                val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
   5.120                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
   5.121                val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
   5.122              in
   5.123                (j + length dts + 1,
   5.124 -               xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2)
   5.125 +               xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
   5.126              end;
   5.127  
   5.128 -          val (_, args1, args2) = List.foldr process_constr (1, [], []) dts;
   5.129 +          val (_, args1, args2) = fold_rev process_constr dts (1, [], []);
   5.130            val Ts = map fastype_of args1;
   5.131            val c = list_comb (Const (cname, Ts ---> T), args1);
   5.132            fun supp t =
     6.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 23:17:35 2009 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 23:58:15 2009 +0100
     6.3 @@ -125,7 +125,7 @@
     6.4  
     6.5      fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
     6.6        let
     6.7 -        fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
     6.8 +        fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
     6.9            let val free1 = mk_Free "x" U j
    6.10            in (case (strip_dtyp dt, strip_type U) of
    6.11               ((_, DtRec m), (Us, _)) =>
    6.12 @@ -141,7 +141,7 @@
    6.13            end;
    6.14  
    6.15          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    6.16 -        val (_, _, prems, t1s, t2s) = List.foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
    6.17 +        val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], [])
    6.18  
    6.19        in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
    6.20          (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
     7.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 23:17:35 2009 +0100
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 23:58:15 2009 +0100
     7.3 @@ -162,8 +162,7 @@
     7.4      val prem' = hd (prems_of exhaustion);
     7.5      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
     7.6      val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
     7.7 -      cterm_of thy (List.foldr (fn ((_, T), t) => Abs ("z", T, t))
     7.8 -        (Bound 0) params))] exhaustion
     7.9 +      cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
    7.10    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    7.11    end;
    7.12  
     8.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 29 23:17:35 2009 +0100
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 29 23:58:15 2009 +0100
     8.3 @@ -313,20 +313,20 @@
     8.4          val (_, fs) = strip_comb comb_t;
     8.5          val used = ["P", "x"] @ (map (fst o dest_Free) fs);
     8.6  
     8.7 -        fun process_constr (((cname, cargs), f), (t1s, t2s)) =
     8.8 +        fun process_constr ((cname, cargs), f) (t1s, t2s) =
     8.9            let
    8.10              val Ts = map (typ_of_dtyp descr' sorts) cargs;
    8.11              val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
    8.12              val eqn = HOLogic.mk_eq (Free ("x", T),
    8.13                list_comb (Const (cname, Ts ---> T), frees));
    8.14              val P' = P $ list_comb (f, frees)
    8.15 -          in ((List.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
    8.16 -                (HOLogic.imp $ eqn $ P') frees)::t1s,
    8.17 -              (List.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
    8.18 -                (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s)
    8.19 +          in (fold_rev (fn Free (s, T) => fn t => HOLogic.mk_all (s, T, t)) frees
    8.20 +                (HOLogic.imp $ eqn $ P') :: t1s,
    8.21 +              fold_rev (fn Free (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees
    8.22 +                (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) :: t2s)
    8.23            end;
    8.24  
    8.25 -        val (t1s, t2s) = List.foldr process_constr ([], []) (constrs ~~ fs);
    8.26 +        val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
    8.27          val lhs = P $ (comb_t $ Free ("x", T))
    8.28        in
    8.29          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
    8.30 @@ -423,9 +423,9 @@
    8.31          val tnames = Name.variant_list ["v"] (make_tnames Ts);
    8.32          val frees = tnames ~~ Ts
    8.33        in
    8.34 -        List.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
    8.35 +        fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
    8.36            (HOLogic.mk_eq (Free ("v", T),
    8.37 -            list_comb (Const (cname, Ts ---> T), map Free frees))) frees
    8.38 +            list_comb (Const (cname, Ts ---> T), map Free frees)))
    8.39        end
    8.40  
    8.41    in map (fn ((_, (_, _, constrs)), T) =>
     9.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Oct 29 23:17:35 2009 +0100
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Oct 29 23:58:15 2009 +0100
     9.3 @@ -138,21 +138,24 @@
     9.4        tname_of (body_type T) mem ["set", "bool"]) ivs);
     9.5      val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
     9.6  
     9.7 -    val prf = List.foldr forall_intr_prf
     9.8 -     (List.foldr (fn ((f, p), prf) =>
     9.9 -        (case head_of (strip_abs_body f) of
    9.10 -           Free (s, T) =>
    9.11 -             let val T' = Logic.varifyT T
    9.12 -             in Abst (s, SOME T', Proofterm.prf_abstract_over
    9.13 -               (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
    9.14 -             end
    9.15 -         | _ => AbsP ("H", SOME p, prf)))
    9.16 -           (Proofterm.proof_combP
    9.17 -             (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2;
    9.18 +    val prf =
    9.19 +      List.foldr forall_intr_prf
    9.20 +        (fold_rev (fn (f, p) => fn prf =>
    9.21 +          (case head_of (strip_abs_body f) of
    9.22 +             Free (s, T) =>
    9.23 +               let val T' = Logic.varifyT T
    9.24 +               in Abst (s, SOME T', Proofterm.prf_abstract_over
    9.25 +                 (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
    9.26 +               end
    9.27 +          | _ => AbsP ("H", SOME p, prf)))
    9.28 +            (rec_fns ~~ prems_of thm)
    9.29 +            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
    9.30  
    9.31 -    val r' = if null is then r else Logic.varify (List.foldr (uncurry lambda)
    9.32 -      r (map Logic.unvarify ivs1 @ filter_out is_unit
    9.33 -          (map (head_of o strip_abs_body) rec_fns)));
    9.34 +    val r' =
    9.35 +      if null is then r
    9.36 +      else Logic.varify (fold_rev lambda
    9.37 +        (map Logic.unvarify ivs1 @ filter_out is_unit
    9.38 +            (map (head_of o strip_abs_body) rec_fns)) r);
    9.39  
    9.40    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    9.41  
    9.42 @@ -200,10 +203,10 @@
    9.43  
    9.44      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    9.45      val prf = forall_intr_prf (y, forall_intr_prf (P,
    9.46 -      List.foldr (fn ((p, r), prf) =>
    9.47 -        forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
    9.48 -          prf))) (Proofterm.proof_combP (prf_of thm',
    9.49 -            map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
    9.50 +      fold_rev (fn (p, r) => fn prf =>
    9.51 +          forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), prf)))
    9.52 +        (prems ~~ rs)
    9.53 +        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
    9.54      val r' = Logic.varify (Abs ("y", T,
    9.55        list_abs (map dest_Free rs, list_comb (r,
    9.56          map Bound ((length rs - 1 downto 0) @ [length rs])))));
    10.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 29 23:17:35 2009 +0100
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 29 23:58:15 2009 +0100
    10.3 @@ -73,8 +73,9 @@
    10.4      val branchT = if null branchTs then HOLogic.unitT
    10.5        else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
    10.6      val arities = remove (op =) 0 (get_arities descr');
    10.7 -    val unneeded_vars = subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
    10.8 -    val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
    10.9 +    val unneeded_vars =
   10.10 +      subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
   10.11 +    val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
   10.12      val recTs = get_rec_types descr' sorts;
   10.13      val newTs = Library.take (length (hd descr), recTs);
   10.14      val oldTs = Library.drop (length (hd descr), recTs);
   10.15 @@ -133,7 +134,7 @@
   10.16        in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
   10.17        end;
   10.18  
   10.19 -    val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
   10.20 +    fun mk_lim t Ts = fold_rev (fn T => fn t => Lim $ mk_fun_inj T (Abs ("x", T, t))) Ts t;
   10.21  
   10.22      (************** generate introduction rules for representing set **********)
   10.23  
   10.24 @@ -143,7 +144,8 @@
   10.25  
   10.26      fun make_intr s n (i, (_, cargs)) =
   10.27        let
   10.28 -        fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of
   10.29 +        fun mk_prem dt (j, prems, ts) =
   10.30 +          (case strip_dtyp dt of
   10.31              (dts, DtRec k) =>
   10.32                let
   10.33                  val Ts = map (typ_of_dtyp descr' sorts) dts;
   10.34 @@ -159,7 +161,7 @@
   10.35                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
   10.36                end);
   10.37  
   10.38 -        val (_, prems, ts) = List.foldr mk_prem (1, [], []) cargs;
   10.39 +        val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []);
   10.40          val concl = HOLogic.mk_Trueprop
   10.41            (Free (s, UnivT') $ mk_univ_inj ts n i)
   10.42        in Logic.list_implies (prems, concl)
   10.43 @@ -213,7 +215,7 @@
   10.44  
   10.45      fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
   10.46        let
   10.47 -        fun constr_arg (dt, (j, l_args, r_args)) =
   10.48 +        fun constr_arg dt (j, l_args, r_args) =
   10.49            let val T = typ_of_dtyp descr' sorts dt;
   10.50                val free_t = mk_Free "x" T j
   10.51            in (case (strip_dtyp dt, strip_type T) of
   10.52 @@ -223,7 +225,7 @@
   10.53              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
   10.54            end;
   10.55  
   10.56 -        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
   10.57 +        val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
   10.58          val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
   10.59          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
   10.60          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
   10.61 @@ -387,7 +389,7 @@
   10.62      val fun_congs = map (fn T => make_elim (Drule.instantiate'
   10.63        [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
   10.64  
   10.65 -    fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
   10.66 +    fun prove_iso_thms ds (inj_thms, elem_thms) =
   10.67        let
   10.68          val (_, (tname, _, _)) = hd ds;
   10.69          val induct = (#induct o the o Symtab.lookup dt_info) tname;
   10.70 @@ -445,8 +447,8 @@
   10.71        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
   10.72        end;
   10.73  
   10.74 -    val (iso_inj_thms_unfolded, iso_elem_thms) = List.foldr prove_iso_thms
   10.75 -      ([], map #3 newT_iso_axms) (tl descr);
   10.76 +    val (iso_inj_thms_unfolded, iso_elem_thms) =
   10.77 +      fold_rev prove_iso_thms (tl descr) ([], map #3 newT_iso_axms);
   10.78      val iso_inj_thms = map snd newT_iso_inj_thms @
   10.79        map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
   10.80  
    11.1 --- a/src/HOL/Tools/Function/size.ML	Thu Oct 29 23:17:35 2009 +0100
    11.2 +++ b/src/HOL/Tools/Function/size.ML	Thu Oct 29 23:58:15 2009 +0100
    11.3 @@ -115,7 +115,7 @@
    11.4            then HOLogic.zero
    11.5            else foldl1 plus (ts @ [HOLogic.Suc_zero])
    11.6        in
    11.7 -        List.foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
    11.8 +        fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
    11.9        end;
   11.10  
   11.11      val fs = maps (fn (_, (name, _, constrs)) =>
    12.1 --- a/src/HOL/Tools/TFL/post.ML	Thu Oct 29 23:17:35 2009 +0100
    12.2 +++ b/src/HOL/Tools/TFL/post.ML	Thu Oct 29 23:58:15 2009 +0100
    12.3 @@ -28,7 +28,7 @@
    12.4   *--------------------------------------------------------------------------*)
    12.5  fun termination_goals rules =
    12.6      map (Type.freeze o HOLogic.dest_Trueprop)
    12.7 -      (List.foldr (fn (th,A) => uncurry (union (op aconv)) (prems_of th, A)) [] rules);
    12.8 +      (fold_rev (union (op aconv) o prems_of) rules []);
    12.9  
   12.10  (*---------------------------------------------------------------------------
   12.11   * Three postprocessors are applied to the definition.  It
    13.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Oct 29 23:17:35 2009 +0100
    13.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu Oct 29 23:58:15 2009 +0100
    13.3 @@ -131,8 +131,7 @@
    13.4  
    13.5  fun FILTER_DISCH_ALL P thm =
    13.6   let fun check tm = P (#t (Thm.rep_cterm tm))
    13.7 - in  List.foldr (fn (tm,th) => if check tm then DISCH tm th else th)
    13.8 -              thm (chyps thm)
    13.9 + in  fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
   13.10   end;
   13.11  
   13.12  (* freezeT expensive! *)
    14.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Oct 29 23:17:35 2009 +0100
    14.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Oct 29 23:58:15 2009 +0100
    14.3 @@ -529,7 +529,7 @@
    14.4                   then writeln (cat_lines ("Extractants =" ::
    14.5                    map (Display.string_of_thm_global thy) extractants))
    14.6                   else ()
    14.7 -     val TCs = List.foldr (uncurry (union (op aconv))) [] TCl
    14.8 +     val TCs = fold_rev (union (op aconv)) TCl []
    14.9       val full_rqt = WFR::TCs
   14.10       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   14.11       val R'abs = S.rand R'
    15.1 --- a/src/HOL/Tools/choice_specification.ML	Thu Oct 29 23:17:35 2009 +0100
    15.2 +++ b/src/HOL/Tools/choice_specification.ML	Thu Oct 29 23:58:15 2009 +0100
    15.3 @@ -120,7 +120,8 @@
    15.4                  val frees = OldTerm.term_frees prop
    15.5                  val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
    15.6                    orelse error "Specificaton: Only free variables of sort 'type' allowed"
    15.7 -                val prop_closed = List.foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
    15.8 +                val prop_closed = fold_rev (fn (vname, T) => fn prop =>
    15.9 +                  HOLogic.mk_all (vname, T, prop)) (map dest_Free frees) prop
   15.10              in
   15.11                  (prop_closed,frees)
   15.12              end
   15.13 @@ -151,7 +152,7 @@
   15.14                    | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)")
   15.15              end
   15.16          val proc_consts = map proc_const consts
   15.17 -        fun mk_exist (c,prop) =
   15.18 +        fun mk_exist c prop =
   15.19              let
   15.20                  val T = type_of c
   15.21                  val cname = Long_Name.base_name (fst (dest_Const c))
   15.22 @@ -161,7 +162,7 @@
   15.23              in
   15.24                  HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop))
   15.25              end
   15.26 -        val ex_prop = List.foldr mk_exist prop proc_consts
   15.27 +        val ex_prop = fold_rev mk_exist proc_consts prop
   15.28          val cnames = map (fst o dest_Const) proc_consts
   15.29          fun post_process (arg as (thy,thm)) =
   15.30              let
    16.1 --- a/src/HOL/Tools/inductive.ML	Thu Oct 29 23:17:35 2009 +0100
    16.2 +++ b/src/HOL/Tools/inductive.ML	Thu Oct 29 23:58:15 2009 +0100
    16.3 @@ -517,16 +517,17 @@
    16.4              | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
    16.5              | _ => (s, NONE)));
    16.6  
    16.7 -        fun mk_prem (s, prems) = (case subst s of
    16.8 -              (_, SOME (t, u)) => t :: u :: prems
    16.9 -            | (t, _) => t :: prems);
   16.10 +        fun mk_prem s prems =
   16.11 +          (case subst s of
   16.12 +            (_, SOME (t, u)) => t :: u :: prems
   16.13 +          | (t, _) => t :: prems);
   16.14  
   16.15          val SOME (_, i, ys, _) = dest_predicate cs params
   16.16            (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
   16.17  
   16.18        in list_all_free (Logic.strip_params r,
   16.19 -        Logic.list_implies (map HOLogic.mk_Trueprop (List.foldr mk_prem
   16.20 -          [] (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r))),
   16.21 +        Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
   16.22 +          (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
   16.23              HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
   16.24        end;
   16.25  
   16.26 @@ -549,9 +550,9 @@
   16.27      (* make predicate for instantiation of abstract induction rule *)
   16.28  
   16.29      val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
   16.30 -      (map_index (fn (i, P) => List.foldr HOLogic.mk_imp
   16.31 -         (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))
   16.32 -         (make_bool_args HOLogic.mk_not I bs i)) preds));
   16.33 +      (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp)
   16.34 +         (make_bool_args HOLogic.mk_not I bs i)
   16.35 +         (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
   16.36  
   16.37      val ind_concl = HOLogic.mk_Trueprop
   16.38        (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
   16.39 @@ -631,9 +632,10 @@
   16.40            map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
   16.41            map (subst o HOLogic.dest_Trueprop)
   16.42              (Logic.strip_assums_hyp r)
   16.43 -      in List.foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
   16.44 -        (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
   16.45 -        (Logic.strip_params r)
   16.46 +      in
   16.47 +        fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
   16.48 +          (Logic.strip_params r)
   16.49 +          (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
   16.50        end
   16.51  
   16.52      (* make a disjunction of all introduction rules *)
    17.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 23:17:35 2009 +0100
    17.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 23:58:15 2009 +0100
    17.3 @@ -71,8 +71,7 @@
    17.4            {intros = intros |>
    17.5             Symtab.update (s, (AList.update Thm.eq_thm_prop
    17.6               (thm, (thyname_of s, nparms)) rules)),
    17.7 -           graph = List.foldr (uncurry (Graph.add_edge o pair s))
    17.8 -             (fold add_node (s :: cs) graph) cs,
    17.9 +           graph = fold_rev (Graph.add_edge o pair s) cs (fold add_node (s :: cs) graph),
   17.10             eqns = eqns} thy
   17.11          end
   17.12      | _ => (warn thm; thy))
    18.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Oct 29 23:17:35 2009 +0100
    18.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Oct 29 23:58:15 2009 +0100
    18.3 @@ -263,8 +263,7 @@
    18.4      val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
    18.5      val rlz'' = fold_rev Logic.all vs2 rlz
    18.6    in (name, (vs,
    18.7 -    if rt = Extraction.nullt then rt else
    18.8 -      List.foldr (uncurry lambda) rt vs1,
    18.9 +    if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
   18.10      ProofRewriteRules.un_hhf_proof rlz' rlz''
   18.11        (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
   18.12    end;
    19.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Oct 29 23:17:35 2009 +0100
    19.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Oct 29 23:58:15 2009 +0100
    19.3 @@ -645,9 +645,9 @@
    19.4  
    19.5  fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
    19.6  let
    19.7 -  fun filter_prems (t, (left, right)) =
    19.8 -    if  p t  then  (left, right @ [t])  else  (left @ right, [])
    19.9 -  val (left, right) = List.foldl filter_prems ([], []) terms
   19.10 +  fun filter_prems t (left, right) =
   19.11 +    if p t then (left, right @ [t]) else (left @ right, [])
   19.12 +  val (left, right) = fold filter_prems terms ([], [])
   19.13  in
   19.14    right @ left
   19.15  end;
    20.1 --- a/src/HOL/Tools/meson.ML	Thu Oct 29 23:17:35 2009 +0100
    20.2 +++ b/src/HOL/Tools/meson.ML	Thu Oct 29 23:58:15 2009 +0100
    20.3 @@ -432,7 +432,7 @@
    20.4  
    20.5  (*Generate Horn clauses for all contrapositives of a clause. The input, th,
    20.6    is a HOL disjunction.*)
    20.7 -fun add_contras crules (th,hcs) =
    20.8 +fun add_contras crules th hcs =
    20.9    let fun rots (0,th) = hcs
   20.10          | rots (k,th) = zero_var_indexes (make_horn crules th) ::
   20.11                          rots(k-1, assoc_right (th RS disj_comm))
   20.12 @@ -443,9 +443,9 @@
   20.13  
   20.14  (*Use "theorem naming" to label the clauses*)
   20.15  fun name_thms label =
   20.16 -    let fun name1 (th, (k,ths)) =
   20.17 +    let fun name1 th (k, ths) =
   20.18            (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
   20.19 -    in  fn ths => #2 (List.foldr name1 (length ths, []) ths)  end;
   20.20 +    in  fn ths => #2 (fold_rev name1 ths (length ths, []))  end;
   20.21  
   20.22  (*Is the given disjunction an all-negative support clause?*)
   20.23  fun is_negative th = forall (not o #1) (literals (prop_of th));
   20.24 @@ -491,9 +491,9 @@
   20.25      TRYALL_eq_assume_tac;
   20.26  
   20.27  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   20.28 -fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   20.29 +fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz;
   20.30  
   20.31 -fun size_of_subgoals st = List.foldr addconcl 0 (prems_of st);
   20.32 +fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0;
   20.33  
   20.34  
   20.35  (*Negation Normal Form*)
   20.36 @@ -553,19 +553,19 @@
   20.37         (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
   20.38          skolemize_nnf_list ctxt ths);
   20.39  
   20.40 -fun add_clauses (th,cls) =
   20.41 +fun add_clauses th cls =
   20.42    let val ctxt0 = Variable.thm_context th
   20.43 -      val (cnfs,ctxt) = make_cnf [] th ctxt0
   20.44 +      val (cnfs, ctxt) = make_cnf [] th ctxt0
   20.45    in Variable.export ctxt ctxt0 cnfs @ cls end;
   20.46  
   20.47  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   20.48    The resulting clauses are HOL disjunctions.*)
   20.49 -fun make_clauses ths = sort_clauses (List.foldr add_clauses [] ths);
   20.50 +fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
   20.51  
   20.52  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
   20.53  fun make_horns ths =
   20.54      name_thms "Horn#"
   20.55 -      (distinct Thm.eq_thm_prop (List.foldr (add_contras clause_rules) [] ths));
   20.56 +      (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths []));
   20.57  
   20.58  (*Could simply use nprems_of, which would count remaining subgoals -- no
   20.59    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
    21.1 --- a/src/HOL/Tools/metis_tools.ML	Thu Oct 29 23:17:35 2009 +0100
    21.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 29 23:58:15 2009 +0100
    21.3 @@ -628,15 +628,14 @@
    21.4          | set_mode FT = FT
    21.5        val mode = set_mode mode0
    21.6        (*transform isabelle clause to metis clause *)
    21.7 -      fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map =
    21.8 +      fun add_thm is_conjecture ith {axioms, tfrees} : logic_map =
    21.9          let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
   21.10          in
   21.11             {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
   21.12              tfrees = union (op =) tfree_lits tfrees}
   21.13          end;
   21.14 -      val lmap0 = List.foldl (add_thm true)
   21.15 -                        {axioms = [], tfrees = init_tfrees ctxt} cls
   21.16 -      val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths
   21.17 +      val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt}
   21.18 +      val lmap = fold (add_thm false) ths (add_tfrees lmap0)
   21.19        val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   21.20        fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
   21.21        (*Now check for the existence of certain combinators*)
   21.22 @@ -647,7 +646,7 @@
   21.23        val thS   = if used "c_COMBS" then [comb_S] else []
   21.24        val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
   21.25        val lmap' = if mode=FO then lmap
   21.26 -                  else List.foldl (add_thm false) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
   21.27 +                  else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
   21.28    in
   21.29        (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
   21.30    end;
    22.1 --- a/src/HOL/Tools/old_primrec.ML	Thu Oct 29 23:17:35 2009 +0100
    22.2 +++ b/src/HOL/Tools/old_primrec.ML	Thu Oct 29 23:58:15 2009 +0100
    22.3 @@ -34,11 +34,11 @@
    22.4    same type in all introduction rules*)
    22.5  fun unify_consts thy cs intr_ts =
    22.6    (let
    22.7 -    fun varify (t, (i, ts)) =
    22.8 +    fun varify t (i, ts) =
    22.9        let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
   22.10        in (maxidx_of_term t', t'::ts) end;
   22.11 -    val (i, cs') = List.foldr varify (~1, []) cs;
   22.12 -    val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
   22.13 +    val (i, cs') = fold_rev varify cs (~1, []);
   22.14 +    val (i', intr_ts') = fold_rev varify intr_ts (i, []);
   22.15      val rec_consts = fold Term.add_consts cs' [];
   22.16      val intr_consts = fold Term.add_consts intr_ts' [];
   22.17      fun unify (cname, cT) =
    23.1 --- a/src/HOL/Tools/refute.ML	Thu Oct 29 23:17:35 2009 +0100
    23.2 +++ b/src/HOL/Tools/refute.ML	Thu Oct 29 23:58:15 2009 +0100
    23.3 @@ -954,7 +954,7 @@
    23.4              (* required for mutually recursive datatypes; those need to   *)
    23.5              (* be added even if they are an instance of an otherwise non- *)
    23.6              (* recursive datatype                                         *)
    23.7 -            fun collect_dtyp (d, acc) =
    23.8 +            fun collect_dtyp d acc =
    23.9              let
   23.10                val dT = typ_of_dtyp descr typ_assoc d
   23.11              in
   23.12 @@ -962,7 +962,7 @@
   23.13                  DatatypeAux.DtTFree _ =>
   23.14                  collect_types dT acc
   23.15                | DatatypeAux.DtType (_, ds) =>
   23.16 -                collect_types dT (List.foldr collect_dtyp acc ds)
   23.17 +                collect_types dT (fold_rev collect_dtyp ds acc)
   23.18                | DatatypeAux.DtRec i =>
   23.19                  if dT mem acc then
   23.20                    acc  (* prevent infinite recursion *)
   23.21 @@ -976,9 +976,9 @@
   23.22                          insert (op =) dT acc
   23.23                        else acc
   23.24                      (* collect argument types *)
   23.25 -                    val acc_dtyps = List.foldr collect_dtyp acc_dT dtyps
   23.26 +                    val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT
   23.27                      (* collect constructor types *)
   23.28 -                    val acc_dconstrs = List.foldr collect_dtyp acc_dtyps (maps snd dconstrs)
   23.29 +                    val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps
   23.30                    in
   23.31                      acc_dconstrs
   23.32                    end
   23.33 @@ -986,7 +986,7 @@
   23.34            in
   23.35              (* argument types 'Ts' could be added here, but they are also *)
   23.36              (* added by 'collect_dtyp' automatically                      *)
   23.37 -            collect_dtyp (DatatypeAux.DtRec index, acc)
   23.38 +            collect_dtyp (DatatypeAux.DtRec index) acc
   23.39            end
   23.40          | NONE =>
   23.41            (* not an inductive datatype, e.g. defined via "typedef" or *)
   23.42 @@ -1596,8 +1596,9 @@
   23.43      val Ts = Term.binder_types (Term.fastype_of t)
   23.44      val t' = Term.incr_boundvars i t
   23.45    in
   23.46 -    List.foldr (fn (T, term) => Abs ("<eta_expand>", T, term))
   23.47 -      (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i))
   23.48 +    fold_rev (fn T => fn term => Abs ("<eta_expand>", T, term))
   23.49 +      (List.take (Ts, i))
   23.50 +      (Term.list_comb (t', map Bound (i-1 downto 0)))
   23.51    end;
   23.52  
   23.53  (* ------------------------------------------------------------------------- *)
   23.54 @@ -2058,7 +2059,7 @@
   23.55              Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
   23.56          in
   23.57            (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *)
   23.58 -          map (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
   23.59 +          map (fn ps => fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) ps
   23.60              HOLogic_empty_set) pairss
   23.61          end
   23.62        | Type (s, Ts) =>
   23.63 @@ -2590,8 +2591,8 @@
   23.64                          (* interpretation list *)
   23.65                          val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs
   23.66                          (* apply 'intr' to all recursive arguments *)
   23.67 -                        val result = List.foldl (fn (arg_i, i) =>
   23.68 -                          interpretation_apply (i, arg_i)) intr arg_intrs
   23.69 +                        val result = fold (fn arg_i => fn i =>
   23.70 +                          interpretation_apply (i, arg_i)) arg_intrs intr
   23.71                          (* update 'REC_OPERATORS' *)
   23.72                          val _ = Array.update (arr, elem, (true, result))
   23.73                        in
   23.74 @@ -2970,11 +2971,11 @@
   23.75              "intersection: interpretation for set is not a node")
   23.76          (* interpretation -> interpretaion *)
   23.77          fun lfp (Node resultsets) =
   23.78 -          List.foldl (fn ((set, resultset), acc) =>
   23.79 +          fold (fn (set, resultset) => fn acc =>
   23.80              if is_subset (resultset, set) then
   23.81                intersection (acc, set)
   23.82              else
   23.83 -              acc) i_univ (i_sets ~~ resultsets)
   23.84 +              acc) (i_sets ~~ resultsets) i_univ
   23.85            | lfp _ =
   23.86              raise REFUTE ("lfp_interpreter",
   23.87                "lfp: interpretation for function is not a node")
   23.88 @@ -3025,11 +3026,11 @@
   23.89              "union: interpretation for set is not a node")
   23.90          (* interpretation -> interpretaion *)
   23.91          fun gfp (Node resultsets) =
   23.92 -          List.foldl (fn ((set, resultset), acc) =>
   23.93 +          fold (fn (set, resultset) => fn acc =>
   23.94              if is_subset (set, resultset) then
   23.95                union (acc, set)
   23.96              else
   23.97 -              acc) i_univ (i_sets ~~ resultsets)
   23.98 +              acc) (i_sets ~~ resultsets) i_univ
   23.99            | gfp _ =
  23.100              raise REFUTE ("gfp_interpreter",
  23.101                "gfp: interpretation for function is not a node")
  23.102 @@ -3127,8 +3128,7 @@
  23.103          val HOLogic_insert    =
  23.104            Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
  23.105        in
  23.106 -        SOME (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
  23.107 -          HOLogic_empty_set pairs)
  23.108 +        SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)
  23.109        end
  23.110      | Type ("prop", [])      =>
  23.111        (case index_from_interpretation intr of
    24.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Oct 29 23:17:35 2009 +0100
    24.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 29 23:58:15 2009 +0100
    24.3 @@ -476,7 +476,7 @@
    24.4        val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
    24.5                                        (map Thm.term_of hyps)
    24.6        val fixed = OldTerm.term_frees (concl_of st) @
    24.7 -                  List.foldl (uncurry (union (op aconv))) [] (map OldTerm.term_frees remaining_hyps)
    24.8 +                  fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
    24.9    in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
   24.10  
   24.11  
    25.1 --- a/src/HOL/Tools/simpdata.ML	Thu Oct 29 23:17:35 2009 +0100
    25.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Oct 29 23:58:15 2009 +0100
    25.3 @@ -64,8 +64,8 @@
    25.4      else
    25.5        let
    25.6          val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
    25.7 -        fun mk_simp_implies Q = List.foldr (fn (R, S) =>
    25.8 -          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
    25.9 +        fun mk_simp_implies Q = fold_rev (fn R => fn S =>
   25.10 +          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Ps Q
   25.11          val aT = TFree ("'a", HOLogic.typeS);
   25.12          val x = Free ("x", aT);
   25.13          val y = Free ("y", aT)
    26.1 --- a/src/Provers/classical.ML	Thu Oct 29 23:17:35 2009 +0100
    26.2 +++ b/src/Provers/classical.ML	Thu Oct 29 23:58:15 2009 +0100
    26.3 @@ -198,10 +198,10 @@
    26.4  (*Uses introduction rules in the normal way, or on negated assumptions,
    26.5    trying rules in order. *)
    26.6  fun swap_res_tac rls =
    26.7 -    let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
    26.8 +    let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
    26.9      in  assume_tac      ORELSE'
   26.10          contr_tac       ORELSE'
   26.11 -        biresolve_tac (List.foldr addrl [] rls)
   26.12 +        biresolve_tac (fold_rev addrl rls [])
   26.13      end;
   26.14  
   26.15  (*Duplication of hazardous rules, for complete provers*)
    27.1 --- a/src/Provers/typedsimp.ML	Thu Oct 29 23:17:35 2009 +0100
    27.2 +++ b/src/Provers/typedsimp.ML	Thu Oct 29 23:58:15 2009 +0100
    27.3 @@ -64,12 +64,12 @@
    27.4  
    27.5  (*If the rule proves an equality then add both forms to simp_rls
    27.6    else add the rule to other_rls*)
    27.7 -fun add_rule (rl, (simp_rls, other_rls)) =
    27.8 +fun add_rule rl (simp_rls, other_rls) =
    27.9      (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
   27.10      handle THM _ => (simp_rls, rl :: other_rls);
   27.11  
   27.12  (*Given the list rls, return the pair (simp_rls, other_rls).*)
   27.13 -fun process_rules rls = List.foldr add_rule ([],[]) rls;
   27.14 +fun process_rules rls = fold_rev add_rule rls ([], []);
   27.15  
   27.16  (*Given list of rewrite rules, return list of both forms, reject others*)
   27.17  fun process_rewrites rls = 
    28.1 --- a/src/Pure/Proof/extraction.ML	Thu Oct 29 23:17:35 2009 +0100
    28.2 +++ b/src/Pure/Proof/extraction.ML	Thu Oct 29 23:58:15 2009 +0100
    28.3 @@ -77,12 +77,12 @@
    28.4  
    28.5  val empty_rules : rules = {next = 0, rs = [], net = Net.empty};
    28.6  
    28.7 -fun add_rule (r as (_, (lhs, _)), {next, rs, net} : rules) =
    28.8 +fun add_rule (r as (_, (lhs, _))) ({next, rs, net} : rules) =
    28.9    {next = next - 1, rs = r :: rs, net = Net.insert_term (K false)
   28.10       (Envir.eta_contract lhs, (next, r)) net};
   28.11  
   28.12  fun merge_rules ({next, rs = rs1, net} : rules) ({rs = rs2, ...} : rules) =
   28.13 -  List.foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
   28.14 +  fold_rev add_rule (subtract (op =) rs1 rs2) {next = next, rs = rs1, net = net};
   28.15  
   28.16  fun condrew thy rules procs =
   28.17    let
   28.18 @@ -231,7 +231,7 @@
   28.19      defs, expand, prep} = ExtractionData.get thy;
   28.20    in
   28.21      ExtractionData.put
   28.22 -      {realizes_eqns = List.foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
   28.23 +      {realizes_eqns = fold_rev add_rule (map (prep_eq thy) eqns) realizes_eqns,
   28.24         typeof_eqns = typeof_eqns, types = types, realizers = realizers,
   28.25         defs = defs, expand = expand, prep = prep} thy
   28.26    end
   28.27 @@ -249,7 +249,7 @@
   28.28    in
   28.29      ExtractionData.put
   28.30        {realizes_eqns = realizes_eqns, realizers = realizers,
   28.31 -       typeof_eqns = List.foldr add_rule typeof_eqns eqns',
   28.32 +       typeof_eqns = fold_rev add_rule eqns' typeof_eqns,
   28.33         types = types, defs = defs, expand = expand, prep = prep} thy
   28.34    end
   28.35  
   28.36 @@ -359,8 +359,8 @@
   28.37    in
   28.38      (ExtractionData.put (if is_def then
   28.39          {realizes_eqns = realizes_eqns,
   28.40 -         typeof_eqns = add_rule (([],
   28.41 -           Logic.dest_equals (prop_of (Drule.abs_def thm))), typeof_eqns),
   28.42 +         typeof_eqns = add_rule ([],
   28.43 +           Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
   28.44           types = types,
   28.45           realizers = realizers, defs = insert Thm.eq_thm thm defs,
   28.46           expand = expand, prep = prep}
   28.47 @@ -458,7 +458,7 @@
   28.48          val vars = vars_of prop;
   28.49          val n = Int.min (length vars, length ts);
   28.50  
   28.51 -        fun add_args ((Var ((a, i), _), t), (vs', tye)) =
   28.52 +        fun add_args (Var ((a, i), _), t) (vs', tye) =
   28.53            if member (op =) rvs a then
   28.54              let val T = etype_of thy' vs Ts t
   28.55              in if T = nullT then (vs', tye)
   28.56 @@ -466,7 +466,7 @@
   28.57              end
   28.58            else (vs', tye)
   28.59  
   28.60 -      in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
   28.61 +      in fold_rev add_args (Library.take (n, vars) ~~ Library.take (n, ts)) ([], []) end;
   28.62  
   28.63      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
   28.64      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
    29.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Oct 29 23:17:35 2009 +0100
    29.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Oct 29 23:58:15 2009 +0100
    29.3 @@ -129,7 +129,7 @@
    29.4        Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
    29.5  
    29.6    (*The function variable for a single constructor*)
    29.7 -  fun add_case (((_, T, _), name, args, _), (opno, cases)) =
    29.8 +  fun add_case ((_, T, _), name, args, _) (opno, cases) =
    29.9      if Syntax.is_identifier name then
   29.10        (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
   29.11      else
   29.12 @@ -138,12 +138,12 @@
   29.13  
   29.14    (*Treatment of a list of constructors, for one part
   29.15      Result adds a list of terms, each a function variable with arguments*)
   29.16 -  fun add_case_list (con_ty_list, (opno, case_lists)) =
   29.17 -    let val (opno', case_list) = List.foldr add_case (opno, []) con_ty_list
   29.18 +  fun add_case_list con_ty_list (opno, case_lists) =
   29.19 +    let val (opno', case_list) = fold_rev add_case con_ty_list (opno, [])
   29.20      in (opno', case_list :: case_lists) end;
   29.21  
   29.22    (*Treatment of all parts*)
   29.23 -  val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists;
   29.24 +  val (_, case_lists) = fold_rev add_case_list con_ty_lists (1, []);
   29.25  
   29.26    (*extract the types of all the variables*)
   29.27    val case_typ = maps (map (#2 o #1)) con_ty_lists ---> @{typ "i => i"};
   29.28 @@ -215,7 +215,7 @@
   29.29    val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
   29.30  
   29.31    (*Treatment of all parts*)
   29.32 -  val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists;
   29.33 +  val (_, recursor_lists) = fold_rev add_case_list rec_ty_lists (1, []);
   29.34  
   29.35    (*extract the types of all the variables*)
   29.36    val recursor_typ = maps (map (#2 o #1)) rec_ty_lists ---> @{typ "i => i"};