# HG changeset patch
# User wenzelm
# Date 1256856595 -3600
# Node ID de76079f973a50098d84ee31c37f365bd474b87e
# Parent  9c3b9bf81e8b71be86fff0180d453240d9742c6a
eliminated some old folds;

diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -526,7 +526,7 @@
 
     fun make_intr s T (cname, cargs) =
       let
-        fun mk_prem (dt, (j, j', prems, ts)) =
+        fun mk_prem dt (j, j', prems, ts) =
           let
             val (dts, dt') = strip_option dt;
             val (dts', dt'') = strip_dtyp dt';
@@ -535,7 +535,7 @@
             val T = typ_of_dtyp descr sorts dt'';
             val free = mk_Free "x" (Us ---> T) j;
             val free' = app_bnds free (length Us);
-            fun mk_abs_fun (T, (i, t)) =
+            fun mk_abs_fun T (i, t) =
               let val U = fastype_of t
               in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
                 Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
@@ -546,10 +546,10 @@
                   HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
                     T --> HOLogic.boolT) $ free')) :: prems
               | _ => prems,
-            snd (List.foldr mk_abs_fun (j', free) Ts) :: ts)
+            snd (fold_rev mk_abs_fun Ts (j', free)) :: ts)
           end;
 
-        val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs;
+        val (_, _, prems, ts) = fold_rev mk_prem cargs (1, 1, [], []);
         val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
           list_comb (Const (cname, map fastype_of ts ---> T), ts))
       in Logic.list_implies (prems, concl)
@@ -710,7 +710,7 @@
 
     (**** constructors ****)
 
-    fun mk_abs_fun (x, t) =
+    fun mk_abs_fun x t =
       let
         val T = fastype_of x;
         val U = fastype_of t
@@ -776,7 +776,7 @@
     fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx))
         (thy, defs, eqns) =
       let
-        fun constr_arg ((dts, dt), (j, l_args, r_args)) =
+        fun constr_arg (dts, dt) (j, l_args, r_args) =
           let
             val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
               (dts ~~ (j upto j + length dts - 1))
@@ -784,16 +784,16 @@
           in
             (j + length dts + 1,
              xs @ x :: l_args,
-             List.foldr mk_abs_fun
+             fold_rev mk_abs_fun xs
                (case dt of
                   DtRec k => if k < length new_type_names then
                       Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
                         typ_of_dtyp descr sorts dt) $ x
                     else error "nested recursion not (yet) supported"
-                | _ => x) xs :: r_args)
+                | _ => x) :: r_args)
           end
 
-        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
+        val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
         val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
         val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
         val constrT = map fastype_of l_args ---> T;
@@ -902,7 +902,7 @@
             let val T = fastype_of t
             in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
 
-          fun constr_arg ((dts, dt), (j, l_args, r_args)) =
+          fun constr_arg (dts, dt) (j, l_args, r_args) =
             let
               val Ts = map (typ_of_dtyp descr'' sorts) dts;
               val xs = map (fn (T, i) => mk_Free "x" T i)
@@ -914,7 +914,7 @@
                map perm (xs @ [x]) @ r_args)
             end
 
-          val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
+          val (_, l_args, r_args) = fold_rev constr_arg dts (1, [], []);
           val c = Const (cname, map fastype_of l_args ---> T)
         in
           Goal.prove_global thy8 [] []
@@ -952,7 +952,7 @@
           val cname = Sign.intern_const thy8
             (Long_Name.append tname (Long_Name.base_name cname));
 
-          fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
+          fun make_inj (dts, dt) (j, args1, args2, eqs) =
             let
               val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
               val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
@@ -963,10 +963,10 @@
               (j + length dts + 1,
                xs @ (x :: args1), ys @ (y :: args2),
                HOLogic.mk_eq
-                 (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs)
+                 (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs)
             end;
 
-          val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts;
+          val (_, args1, args2, eqs) = fold_rev make_inj dts (1, [], [], []);
           val Ts = map fastype_of args1;
           val c = Const (cname, Ts ---> T)
         in
@@ -995,17 +995,17 @@
             (Long_Name.append tname (Long_Name.base_name cname));
           val atomT = Type (atom, []);
 
-          fun process_constr ((dts, dt), (j, args1, args2)) =
+          fun process_constr (dts, dt) (j, args1, args2) =
             let
               val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
               val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
               val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
             in
               (j + length dts + 1,
-               xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2)
+               xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
             end;
 
-          val (_, args1, args2) = List.foldr process_constr (1, [], []) dts;
+          val (_, args1, args2) = fold_rev process_constr dts (1, [], []);
           val Ts = map fastype_of args1;
           val c = list_comb (Const (cname, Ts ---> T), args1);
           fun supp t =
diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -125,7 +125,7 @@
 
     fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
       let
-        fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
+        fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
           let val free1 = mk_Free "x" U j
           in (case (strip_dtyp dt, strip_type U) of
              ((_, DtRec m), (Us, _)) =>
@@ -141,7 +141,7 @@
           end;
 
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val (_, _, prems, t1s, t2s) = List.foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
+        val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], [])
 
       in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
         (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -162,8 +162,7 @@
     val prem' = hd (prems_of exhaustion);
     val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
     val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
-      cterm_of thy (List.foldr (fn ((_, T), t) => Abs ("z", T, t))
-        (Bound 0) params))] exhaustion
+      cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
   in compose_tac (false, exhaustion', nprems_of exhaustion) i state
   end;
 
diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -313,20 +313,20 @@
         val (_, fs) = strip_comb comb_t;
         val used = ["P", "x"] @ (map (fst o dest_Free) fs);
 
-        fun process_constr (((cname, cargs), f), (t1s, t2s)) =
+        fun process_constr ((cname, cargs), f) (t1s, t2s) =
           let
             val Ts = map (typ_of_dtyp descr' sorts) cargs;
             val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
             val eqn = HOLogic.mk_eq (Free ("x", T),
               list_comb (Const (cname, Ts ---> T), frees));
             val P' = P $ list_comb (f, frees)
-          in ((List.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
-                (HOLogic.imp $ eqn $ P') frees)::t1s,
-              (List.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
-                (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s)
+          in (fold_rev (fn Free (s, T) => fn t => HOLogic.mk_all (s, T, t)) frees
+                (HOLogic.imp $ eqn $ P') :: t1s,
+              fold_rev (fn Free (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees
+                (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) :: t2s)
           end;
 
-        val (t1s, t2s) = List.foldr process_constr ([], []) (constrs ~~ fs);
+        val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
         val lhs = P $ (comb_t $ Free ("x", T))
       in
         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
@@ -423,9 +423,9 @@
         val tnames = Name.variant_list ["v"] (make_tnames Ts);
         val frees = tnames ~~ Ts
       in
-        List.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
+        fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
           (HOLogic.mk_eq (Free ("v", T),
-            list_comb (Const (cname, Ts ---> T), map Free frees))) frees
+            list_comb (Const (cname, Ts ---> T), map Free frees)))
       end
 
   in map (fn ((_, (_, _, constrs)), T) =>
diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -138,21 +138,24 @@
       tname_of (body_type T) mem ["set", "bool"]) ivs);
     val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
 
-    val prf = List.foldr forall_intr_prf
-     (List.foldr (fn ((f, p), prf) =>
-        (case head_of (strip_abs_body f) of
-           Free (s, T) =>
-             let val T' = Logic.varifyT T
-             in Abst (s, SOME T', Proofterm.prf_abstract_over
-               (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
-             end
-         | _ => AbsP ("H", SOME p, prf)))
-           (Proofterm.proof_combP
-             (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2;
+    val prf =
+      List.foldr forall_intr_prf
+        (fold_rev (fn (f, p) => fn prf =>
+          (case head_of (strip_abs_body f) of
+             Free (s, T) =>
+               let val T' = Logic.varifyT T
+               in Abst (s, SOME T', Proofterm.prf_abstract_over
+                 (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
+               end
+          | _ => AbsP ("H", SOME p, prf)))
+            (rec_fns ~~ prems_of thm)
+            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
 
-    val r' = if null is then r else Logic.varify (List.foldr (uncurry lambda)
-      r (map Logic.unvarify ivs1 @ filter_out is_unit
-          (map (head_of o strip_abs_body) rec_fns)));
+    val r' =
+      if null is then r
+      else Logic.varify (fold_rev lambda
+        (map Logic.unvarify ivs1 @ filter_out is_unit
+            (map (head_of o strip_abs_body) rec_fns)) r);
 
   in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
 
@@ -200,10 +203,10 @@
 
     val P = Var (("P", 0), rT' --> HOLogic.boolT);
     val prf = forall_intr_prf (y, forall_intr_prf (P,
-      List.foldr (fn ((p, r), prf) =>
-        forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
-          prf))) (Proofterm.proof_combP (prf_of thm',
-            map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
+      fold_rev (fn (p, r) => fn prf =>
+          forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), prf)))
+        (prems ~~ rs)
+        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
     val r' = Logic.varify (Abs ("y", T,
       list_abs (map dest_Free rs, list_comb (r,
         map Bound ((length rs - 1 downto 0) @ [length rs])))));
diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -73,8 +73,9 @@
     val branchT = if null branchTs then HOLogic.unitT
       else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     val arities = remove (op =) 0 (get_arities descr');
-    val unneeded_vars = subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
-    val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
+    val unneeded_vars =
+      subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
+    val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
     val recTs = get_rec_types descr' sorts;
     val newTs = Library.take (length (hd descr), recTs);
     val oldTs = Library.drop (length (hd descr), recTs);
@@ -133,7 +134,7 @@
       in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
       end;
 
-    val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
+    fun mk_lim t Ts = fold_rev (fn T => fn t => Lim $ mk_fun_inj T (Abs ("x", T, t))) Ts t;
 
     (************** generate introduction rules for representing set **********)
 
@@ -143,7 +144,8 @@
 
     fun make_intr s n (i, (_, cargs)) =
       let
-        fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of
+        fun mk_prem dt (j, prems, ts) =
+          (case strip_dtyp dt of
             (dts, DtRec k) =>
               let
                 val Ts = map (typ_of_dtyp descr' sorts) dts;
@@ -159,7 +161,7 @@
               in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
               end);
 
-        val (_, prems, ts) = List.foldr mk_prem (1, [], []) cargs;
+        val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []);
         val concl = HOLogic.mk_Trueprop
           (Free (s, UnivT') $ mk_univ_inj ts n i)
       in Logic.list_implies (prems, concl)
@@ -213,7 +215,7 @@
 
     fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
       let
-        fun constr_arg (dt, (j, l_args, r_args)) =
+        fun constr_arg dt (j, l_args, r_args) =
           let val T = typ_of_dtyp descr' sorts dt;
               val free_t = mk_Free "x" T j
           in (case (strip_dtyp dt, strip_type T) of
@@ -223,7 +225,7 @@
             | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
           end;
 
-        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
+        val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
         val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
         val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
         val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
@@ -387,7 +389,7 @@
     val fun_congs = map (fn T => make_elim (Drule.instantiate'
       [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
 
-    fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
+    fun prove_iso_thms ds (inj_thms, elem_thms) =
       let
         val (_, (tname, _, _)) = hd ds;
         val induct = (#induct o the o Symtab.lookup dt_info) tname;
@@ -445,8 +447,8 @@
       in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
       end;
 
-    val (iso_inj_thms_unfolded, iso_elem_thms) = List.foldr prove_iso_thms
-      ([], map #3 newT_iso_axms) (tl descr);
+    val (iso_inj_thms_unfolded, iso_elem_thms) =
+      fold_rev prove_iso_thms (tl descr) ([], map #3 newT_iso_axms);
     val iso_inj_thms = map snd newT_iso_inj_thms @
       map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
 
diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -517,16 +517,17 @@
             | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
             | _ => (s, NONE)));
 
-        fun mk_prem (s, prems) = (case subst s of
-              (_, SOME (t, u)) => t :: u :: prems
-            | (t, _) => t :: prems);
+        fun mk_prem s prems =
+          (case subst s of
+            (_, SOME (t, u)) => t :: u :: prems
+          | (t, _) => t :: prems);
 
         val SOME (_, i, ys, _) = dest_predicate cs params
           (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
 
       in list_all_free (Logic.strip_params r,
-        Logic.list_implies (map HOLogic.mk_Trueprop (List.foldr mk_prem
-          [] (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r))),
+        Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
+          (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
             HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
       end;
 
@@ -549,9 +550,9 @@
     (* make predicate for instantiation of abstract induction rule *)
 
     val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
-      (map_index (fn (i, P) => List.foldr HOLogic.mk_imp
-         (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))
-         (make_bool_args HOLogic.mk_not I bs i)) preds));
+      (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp)
+         (make_bool_args HOLogic.mk_not I bs i)
+         (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
 
     val ind_concl = HOLogic.mk_Trueprop
       (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
@@ -631,9 +632,10 @@
           map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
           map (subst o HOLogic.dest_Trueprop)
             (Logic.strip_assums_hyp r)
-      in List.foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
-        (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
-        (Logic.strip_params r)
+      in
+        fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
+          (Logic.strip_params r)
+          (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
       end
 
     (* make a disjunction of all introduction rules *)
diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -71,8 +71,7 @@
           {intros = intros |>
            Symtab.update (s, (AList.update Thm.eq_thm_prop
              (thm, (thyname_of s, nparms)) rules)),
-           graph = List.foldr (uncurry (Graph.add_edge o pair s))
-             (fold add_node (s :: cs) graph) cs,
+           graph = fold_rev (Graph.add_edge o pair s) cs (fold add_node (s :: cs) graph),
            eqns = eqns} thy
         end
     | _ => (warn thm; thy))
diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -263,8 +263,7 @@
     val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
     val rlz'' = fold_rev Logic.all vs2 rlz
   in (name, (vs,
-    if rt = Extraction.nullt then rt else
-      List.foldr (uncurry lambda) rt vs1,
+    if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
     ProofRewriteRules.un_hhf_proof rlz' rlz''
       (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
   end;
diff -r 9c3b9bf81e8b -r de76079f973a src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Thu Oct 29 23:48:56 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML	Thu Oct 29 23:49:55 2009 +0100
@@ -34,11 +34,11 @@
   same type in all introduction rules*)
 fun unify_consts thy cs intr_ts =
   (let
-    fun varify (t, (i, ts)) =
+    fun varify t (i, ts) =
       let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
       in (maxidx_of_term t', t'::ts) end;
-    val (i, cs') = List.foldr varify (~1, []) cs;
-    val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
+    val (i, cs') = fold_rev varify cs (~1, []);
+    val (i', intr_ts') = fold_rev varify intr_ts (i, []);
     val rec_consts = fold Term.add_consts cs' [];
     val intr_consts = fold Term.add_consts intr_ts' [];
     fun unify (cname, cT) =