eliminated some old folds;
authorwenzelm
Thu Oct 29 23:49:55 2009 +0100 (2009-10-29)
changeset 33338de76079f973a
parent 33337 9c3b9bf81e8b
child 33339 d41f77196338
eliminated some old folds;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/old_primrec.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 23:48:56 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 23:49:55 2009 +0100
     1.3 @@ -526,7 +526,7 @@
     1.4  
     1.5      fun make_intr s T (cname, cargs) =
     1.6        let
     1.7 -        fun mk_prem (dt, (j, j', prems, ts)) =
     1.8 +        fun mk_prem dt (j, j', prems, ts) =
     1.9            let
    1.10              val (dts, dt') = strip_option dt;
    1.11              val (dts', dt'') = strip_dtyp dt';
    1.12 @@ -535,7 +535,7 @@
    1.13              val T = typ_of_dtyp descr sorts dt'';
    1.14              val free = mk_Free "x" (Us ---> T) j;
    1.15              val free' = app_bnds free (length Us);
    1.16 -            fun mk_abs_fun (T, (i, t)) =
    1.17 +            fun mk_abs_fun T (i, t) =
    1.18                let val U = fastype_of t
    1.19                in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
    1.20                  Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
    1.21 @@ -546,10 +546,10 @@
    1.22                    HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
    1.23                      T --> HOLogic.boolT) $ free')) :: prems
    1.24                | _ => prems,
    1.25 -            snd (List.foldr mk_abs_fun (j', free) Ts) :: ts)
    1.26 +            snd (fold_rev mk_abs_fun Ts (j', free)) :: ts)
    1.27            end;
    1.28  
    1.29 -        val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs;
    1.30 +        val (_, _, prems, ts) = fold_rev mk_prem cargs (1, 1, [], []);
    1.31          val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
    1.32            list_comb (Const (cname, map fastype_of ts ---> T), ts))
    1.33        in Logic.list_implies (prems, concl)
    1.34 @@ -710,7 +710,7 @@
    1.35  
    1.36      (**** constructors ****)
    1.37  
    1.38 -    fun mk_abs_fun (x, t) =
    1.39 +    fun mk_abs_fun x t =
    1.40        let
    1.41          val T = fastype_of x;
    1.42          val U = fastype_of t
    1.43 @@ -776,7 +776,7 @@
    1.44      fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx))
    1.45          (thy, defs, eqns) =
    1.46        let
    1.47 -        fun constr_arg ((dts, dt), (j, l_args, r_args)) =
    1.48 +        fun constr_arg (dts, dt) (j, l_args, r_args) =
    1.49            let
    1.50              val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
    1.51                (dts ~~ (j upto j + length dts - 1))
    1.52 @@ -784,16 +784,16 @@
    1.53            in
    1.54              (j + length dts + 1,
    1.55               xs @ x :: l_args,
    1.56 -             List.foldr mk_abs_fun
    1.57 +             fold_rev mk_abs_fun xs
    1.58                 (case dt of
    1.59                    DtRec k => if k < length new_type_names then
    1.60                        Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
    1.61                          typ_of_dtyp descr sorts dt) $ x
    1.62                      else error "nested recursion not (yet) supported"
    1.63 -                | _ => x) xs :: r_args)
    1.64 +                | _ => x) :: r_args)
    1.65            end
    1.66  
    1.67 -        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
    1.68 +        val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
    1.69          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
    1.70          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
    1.71          val constrT = map fastype_of l_args ---> T;
    1.72 @@ -902,7 +902,7 @@
    1.73              let val T = fastype_of t
    1.74              in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
    1.75  
    1.76 -          fun constr_arg ((dts, dt), (j, l_args, r_args)) =
    1.77 +          fun constr_arg (dts, dt) (j, l_args, r_args) =
    1.78              let
    1.79                val Ts = map (typ_of_dtyp descr'' sorts) dts;
    1.80                val xs = map (fn (T, i) => mk_Free "x" T i)
    1.81 @@ -914,7 +914,7 @@
    1.82                 map perm (xs @ [x]) @ r_args)
    1.83              end
    1.84  
    1.85 -          val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
    1.86 +          val (_, l_args, r_args) = fold_rev constr_arg dts (1, [], []);
    1.87            val c = Const (cname, map fastype_of l_args ---> T)
    1.88          in
    1.89            Goal.prove_global thy8 [] []
    1.90 @@ -952,7 +952,7 @@
    1.91            val cname = Sign.intern_const thy8
    1.92              (Long_Name.append tname (Long_Name.base_name cname));
    1.93  
    1.94 -          fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
    1.95 +          fun make_inj (dts, dt) (j, args1, args2, eqs) =
    1.96              let
    1.97                val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
    1.98                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
    1.99 @@ -963,10 +963,10 @@
   1.100                (j + length dts + 1,
   1.101                 xs @ (x :: args1), ys @ (y :: args2),
   1.102                 HOLogic.mk_eq
   1.103 -                 (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs)
   1.104 +                 (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs)
   1.105              end;
   1.106  
   1.107 -          val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts;
   1.108 +          val (_, args1, args2, eqs) = fold_rev make_inj dts (1, [], [], []);
   1.109            val Ts = map fastype_of args1;
   1.110            val c = Const (cname, Ts ---> T)
   1.111          in
   1.112 @@ -995,17 +995,17 @@
   1.113              (Long_Name.append tname (Long_Name.base_name cname));
   1.114            val atomT = Type (atom, []);
   1.115  
   1.116 -          fun process_constr ((dts, dt), (j, args1, args2)) =
   1.117 +          fun process_constr (dts, dt) (j, args1, args2) =
   1.118              let
   1.119                val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
   1.120                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
   1.121                val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
   1.122              in
   1.123                (j + length dts + 1,
   1.124 -               xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2)
   1.125 +               xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
   1.126              end;
   1.127  
   1.128 -          val (_, args1, args2) = List.foldr process_constr (1, [], []) dts;
   1.129 +          val (_, args1, args2) = fold_rev process_constr dts (1, [], []);
   1.130            val Ts = map fastype_of args1;
   1.131            val c = list_comb (Const (cname, Ts ---> T), args1);
   1.132            fun supp t =
     2.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 23:48:56 2009 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 23:49:55 2009 +0100
     2.3 @@ -125,7 +125,7 @@
     2.4  
     2.5      fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
     2.6        let
     2.7 -        fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
     2.8 +        fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
     2.9            let val free1 = mk_Free "x" U j
    2.10            in (case (strip_dtyp dt, strip_type U) of
    2.11               ((_, DtRec m), (Us, _)) =>
    2.12 @@ -141,7 +141,7 @@
    2.13            end;
    2.14  
    2.15          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    2.16 -        val (_, _, prems, t1s, t2s) = List.foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
    2.17 +        val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], [])
    2.18  
    2.19        in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
    2.20          (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
     3.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 23:48:56 2009 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 23:49:55 2009 +0100
     3.3 @@ -162,8 +162,7 @@
     3.4      val prem' = hd (prems_of exhaustion);
     3.5      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
     3.6      val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
     3.7 -      cterm_of thy (List.foldr (fn ((_, T), t) => Abs ("z", T, t))
     3.8 -        (Bound 0) params))] exhaustion
     3.9 +      cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
    3.10    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    3.11    end;
    3.12  
     4.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 29 23:48:56 2009 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 29 23:49:55 2009 +0100
     4.3 @@ -313,20 +313,20 @@
     4.4          val (_, fs) = strip_comb comb_t;
     4.5          val used = ["P", "x"] @ (map (fst o dest_Free) fs);
     4.6  
     4.7 -        fun process_constr (((cname, cargs), f), (t1s, t2s)) =
     4.8 +        fun process_constr ((cname, cargs), f) (t1s, t2s) =
     4.9            let
    4.10              val Ts = map (typ_of_dtyp descr' sorts) cargs;
    4.11              val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
    4.12              val eqn = HOLogic.mk_eq (Free ("x", T),
    4.13                list_comb (Const (cname, Ts ---> T), frees));
    4.14              val P' = P $ list_comb (f, frees)
    4.15 -          in ((List.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
    4.16 -                (HOLogic.imp $ eqn $ P') frees)::t1s,
    4.17 -              (List.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
    4.18 -                (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s)
    4.19 +          in (fold_rev (fn Free (s, T) => fn t => HOLogic.mk_all (s, T, t)) frees
    4.20 +                (HOLogic.imp $ eqn $ P') :: t1s,
    4.21 +              fold_rev (fn Free (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees
    4.22 +                (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) :: t2s)
    4.23            end;
    4.24  
    4.25 -        val (t1s, t2s) = List.foldr process_constr ([], []) (constrs ~~ fs);
    4.26 +        val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
    4.27          val lhs = P $ (comb_t $ Free ("x", T))
    4.28        in
    4.29          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
    4.30 @@ -423,9 +423,9 @@
    4.31          val tnames = Name.variant_list ["v"] (make_tnames Ts);
    4.32          val frees = tnames ~~ Ts
    4.33        in
    4.34 -        List.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
    4.35 +        fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
    4.36            (HOLogic.mk_eq (Free ("v", T),
    4.37 -            list_comb (Const (cname, Ts ---> T), map Free frees))) frees
    4.38 +            list_comb (Const (cname, Ts ---> T), map Free frees)))
    4.39        end
    4.40  
    4.41    in map (fn ((_, (_, _, constrs)), T) =>
     5.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Oct 29 23:48:56 2009 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Oct 29 23:49:55 2009 +0100
     5.3 @@ -138,21 +138,24 @@
     5.4        tname_of (body_type T) mem ["set", "bool"]) ivs);
     5.5      val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
     5.6  
     5.7 -    val prf = List.foldr forall_intr_prf
     5.8 -     (List.foldr (fn ((f, p), prf) =>
     5.9 -        (case head_of (strip_abs_body f) of
    5.10 -           Free (s, T) =>
    5.11 -             let val T' = Logic.varifyT T
    5.12 -             in Abst (s, SOME T', Proofterm.prf_abstract_over
    5.13 -               (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
    5.14 -             end
    5.15 -         | _ => AbsP ("H", SOME p, prf)))
    5.16 -           (Proofterm.proof_combP
    5.17 -             (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2;
    5.18 +    val prf =
    5.19 +      List.foldr forall_intr_prf
    5.20 +        (fold_rev (fn (f, p) => fn prf =>
    5.21 +          (case head_of (strip_abs_body f) of
    5.22 +             Free (s, T) =>
    5.23 +               let val T' = Logic.varifyT T
    5.24 +               in Abst (s, SOME T', Proofterm.prf_abstract_over
    5.25 +                 (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
    5.26 +               end
    5.27 +          | _ => AbsP ("H", SOME p, prf)))
    5.28 +            (rec_fns ~~ prems_of thm)
    5.29 +            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
    5.30  
    5.31 -    val r' = if null is then r else Logic.varify (List.foldr (uncurry lambda)
    5.32 -      r (map Logic.unvarify ivs1 @ filter_out is_unit
    5.33 -          (map (head_of o strip_abs_body) rec_fns)));
    5.34 +    val r' =
    5.35 +      if null is then r
    5.36 +      else Logic.varify (fold_rev lambda
    5.37 +        (map Logic.unvarify ivs1 @ filter_out is_unit
    5.38 +            (map (head_of o strip_abs_body) rec_fns)) r);
    5.39  
    5.40    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    5.41  
    5.42 @@ -200,10 +203,10 @@
    5.43  
    5.44      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    5.45      val prf = forall_intr_prf (y, forall_intr_prf (P,
    5.46 -      List.foldr (fn ((p, r), prf) =>
    5.47 -        forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
    5.48 -          prf))) (Proofterm.proof_combP (prf_of thm',
    5.49 -            map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
    5.50 +      fold_rev (fn (p, r) => fn prf =>
    5.51 +          forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), prf)))
    5.52 +        (prems ~~ rs)
    5.53 +        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
    5.54      val r' = Logic.varify (Abs ("y", T,
    5.55        list_abs (map dest_Free rs, list_comb (r,
    5.56          map Bound ((length rs - 1 downto 0) @ [length rs])))));
     6.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 29 23:48:56 2009 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 29 23:49:55 2009 +0100
     6.3 @@ -73,8 +73,9 @@
     6.4      val branchT = if null branchTs then HOLogic.unitT
     6.5        else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     6.6      val arities = remove (op =) 0 (get_arities descr');
     6.7 -    val unneeded_vars = subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
     6.8 -    val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
     6.9 +    val unneeded_vars =
    6.10 +      subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
    6.11 +    val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
    6.12      val recTs = get_rec_types descr' sorts;
    6.13      val newTs = Library.take (length (hd descr), recTs);
    6.14      val oldTs = Library.drop (length (hd descr), recTs);
    6.15 @@ -133,7 +134,7 @@
    6.16        in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
    6.17        end;
    6.18  
    6.19 -    val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
    6.20 +    fun mk_lim t Ts = fold_rev (fn T => fn t => Lim $ mk_fun_inj T (Abs ("x", T, t))) Ts t;
    6.21  
    6.22      (************** generate introduction rules for representing set **********)
    6.23  
    6.24 @@ -143,7 +144,8 @@
    6.25  
    6.26      fun make_intr s n (i, (_, cargs)) =
    6.27        let
    6.28 -        fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of
    6.29 +        fun mk_prem dt (j, prems, ts) =
    6.30 +          (case strip_dtyp dt of
    6.31              (dts, DtRec k) =>
    6.32                let
    6.33                  val Ts = map (typ_of_dtyp descr' sorts) dts;
    6.34 @@ -159,7 +161,7 @@
    6.35                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
    6.36                end);
    6.37  
    6.38 -        val (_, prems, ts) = List.foldr mk_prem (1, [], []) cargs;
    6.39 +        val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []);
    6.40          val concl = HOLogic.mk_Trueprop
    6.41            (Free (s, UnivT') $ mk_univ_inj ts n i)
    6.42        in Logic.list_implies (prems, concl)
    6.43 @@ -213,7 +215,7 @@
    6.44  
    6.45      fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
    6.46        let
    6.47 -        fun constr_arg (dt, (j, l_args, r_args)) =
    6.48 +        fun constr_arg dt (j, l_args, r_args) =
    6.49            let val T = typ_of_dtyp descr' sorts dt;
    6.50                val free_t = mk_Free "x" T j
    6.51            in (case (strip_dtyp dt, strip_type T) of
    6.52 @@ -223,7 +225,7 @@
    6.53              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
    6.54            end;
    6.55  
    6.56 -        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
    6.57 +        val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
    6.58          val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
    6.59          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
    6.60          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
    6.61 @@ -387,7 +389,7 @@
    6.62      val fun_congs = map (fn T => make_elim (Drule.instantiate'
    6.63        [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
    6.64  
    6.65 -    fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
    6.66 +    fun prove_iso_thms ds (inj_thms, elem_thms) =
    6.67        let
    6.68          val (_, (tname, _, _)) = hd ds;
    6.69          val induct = (#induct o the o Symtab.lookup dt_info) tname;
    6.70 @@ -445,8 +447,8 @@
    6.71        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
    6.72        end;
    6.73  
    6.74 -    val (iso_inj_thms_unfolded, iso_elem_thms) = List.foldr prove_iso_thms
    6.75 -      ([], map #3 newT_iso_axms) (tl descr);
    6.76 +    val (iso_inj_thms_unfolded, iso_elem_thms) =
    6.77 +      fold_rev prove_iso_thms (tl descr) ([], map #3 newT_iso_axms);
    6.78      val iso_inj_thms = map snd newT_iso_inj_thms @
    6.79        map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
    6.80  
     7.1 --- a/src/HOL/Tools/inductive.ML	Thu Oct 29 23:48:56 2009 +0100
     7.2 +++ b/src/HOL/Tools/inductive.ML	Thu Oct 29 23:49:55 2009 +0100
     7.3 @@ -517,16 +517,17 @@
     7.4              | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
     7.5              | _ => (s, NONE)));
     7.6  
     7.7 -        fun mk_prem (s, prems) = (case subst s of
     7.8 -              (_, SOME (t, u)) => t :: u :: prems
     7.9 -            | (t, _) => t :: prems);
    7.10 +        fun mk_prem s prems =
    7.11 +          (case subst s of
    7.12 +            (_, SOME (t, u)) => t :: u :: prems
    7.13 +          | (t, _) => t :: prems);
    7.14  
    7.15          val SOME (_, i, ys, _) = dest_predicate cs params
    7.16            (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
    7.17  
    7.18        in list_all_free (Logic.strip_params r,
    7.19 -        Logic.list_implies (map HOLogic.mk_Trueprop (List.foldr mk_prem
    7.20 -          [] (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r))),
    7.21 +        Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
    7.22 +          (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
    7.23              HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
    7.24        end;
    7.25  
    7.26 @@ -549,9 +550,9 @@
    7.27      (* make predicate for instantiation of abstract induction rule *)
    7.28  
    7.29      val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
    7.30 -      (map_index (fn (i, P) => List.foldr HOLogic.mk_imp
    7.31 -         (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))
    7.32 -         (make_bool_args HOLogic.mk_not I bs i)) preds));
    7.33 +      (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp)
    7.34 +         (make_bool_args HOLogic.mk_not I bs i)
    7.35 +         (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
    7.36  
    7.37      val ind_concl = HOLogic.mk_Trueprop
    7.38        (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
    7.39 @@ -631,9 +632,10 @@
    7.40            map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
    7.41            map (subst o HOLogic.dest_Trueprop)
    7.42              (Logic.strip_assums_hyp r)
    7.43 -      in List.foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
    7.44 -        (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
    7.45 -        (Logic.strip_params r)
    7.46 +      in
    7.47 +        fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
    7.48 +          (Logic.strip_params r)
    7.49 +          (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
    7.50        end
    7.51  
    7.52      (* make a disjunction of all introduction rules *)
     8.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 23:48:56 2009 +0100
     8.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 23:49:55 2009 +0100
     8.3 @@ -71,8 +71,7 @@
     8.4            {intros = intros |>
     8.5             Symtab.update (s, (AList.update Thm.eq_thm_prop
     8.6               (thm, (thyname_of s, nparms)) rules)),
     8.7 -           graph = List.foldr (uncurry (Graph.add_edge o pair s))
     8.8 -             (fold add_node (s :: cs) graph) cs,
     8.9 +           graph = fold_rev (Graph.add_edge o pair s) cs (fold add_node (s :: cs) graph),
    8.10             eqns = eqns} thy
    8.11          end
    8.12      | _ => (warn thm; thy))
     9.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Oct 29 23:48:56 2009 +0100
     9.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Oct 29 23:49:55 2009 +0100
     9.3 @@ -263,8 +263,7 @@
     9.4      val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
     9.5      val rlz'' = fold_rev Logic.all vs2 rlz
     9.6    in (name, (vs,
     9.7 -    if rt = Extraction.nullt then rt else
     9.8 -      List.foldr (uncurry lambda) rt vs1,
     9.9 +    if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
    9.10      ProofRewriteRules.un_hhf_proof rlz' rlz''
    9.11        (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
    9.12    end;
    10.1 --- a/src/HOL/Tools/old_primrec.ML	Thu Oct 29 23:48:56 2009 +0100
    10.2 +++ b/src/HOL/Tools/old_primrec.ML	Thu Oct 29 23:49:55 2009 +0100
    10.3 @@ -34,11 +34,11 @@
    10.4    same type in all introduction rules*)
    10.5  fun unify_consts thy cs intr_ts =
    10.6    (let
    10.7 -    fun varify (t, (i, ts)) =
    10.8 +    fun varify t (i, ts) =
    10.9        let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
   10.10        in (maxidx_of_term t', t'::ts) end;
   10.11 -    val (i, cs') = List.foldr varify (~1, []) cs;
   10.12 -    val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
   10.13 +    val (i, cs') = fold_rev varify cs (~1, []);
   10.14 +    val (i', intr_ts') = fold_rev varify intr_ts (i, []);
   10.15      val rec_consts = fold Term.add_consts cs' [];
   10.16      val intr_consts = fold Term.add_consts intr_ts' [];
   10.17      fun unify (cname, cT) =