src/HOL/Tools/refute.ML

                 ^ Syntax.string_of_typ_global thy T ^ ") is not a variable")
             else ()
             (* required for mutually recursive datatypes; those need to   *)
             (* be added even if they are an instance of an otherwise non- *)
             (* recursive datatype                                         *)
-            fun collect_dtyp (d, acc) =
+            fun collect_dtyp d acc =
             let
               val dT = typ_of_dtyp descr typ_assoc d
             in
               case d of
                 DatatypeAux.DtTFree _ =>
                 collect_types dT acc
               | DatatypeAux.DtType (_, ds) =>
-                collect_types dT (List.foldr collect_dtyp acc ds)
+                collect_types dT (fold_rev collect_dtyp ds acc)
               | DatatypeAux.DtRec i =>
                 if dT mem acc then
                   acc  (* prevent infinite recursion *)
                 else
                   let

                     val acc_dT = if Library.exists (fn (_, ds) =>
                       Library.exists DatatypeAux.is_rec_type ds) dconstrs then
                         insert (op =) dT acc
                       else acc
                     (* collect argument types *)
-                    val acc_dtyps = List.foldr collect_dtyp acc_dT dtyps
+                    val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT
                     (* collect constructor types *)
-                    val acc_dconstrs = List.foldr collect_dtyp acc_dtyps (maps snd dconstrs)
+                    val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps
                   in
                     acc_dconstrs
                   end
             end
           in
             (* argument types 'Ts' could be added here, but they are also *)
             (* added by 'collect_dtyp' automatically                      *)
-            collect_dtyp (DatatypeAux.DtRec index, acc)
+            collect_dtyp (DatatypeAux.DtRec index) acc
           end
         | NONE =>
           (* not an inductive datatype, e.g. defined via "typedef" or *)
           (* "typedecl"                                               *)
           insert (op =) T (fold collect_types Ts acc))

   fun eta_expand t i =
   let
     val Ts = Term.binder_types (Term.fastype_of t)
     val t' = Term.incr_boundvars i t
   in
-    List.foldr (fn (T, term) => Abs ("<eta_expand>", T, term))
-      (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i))
+    fold_rev (fn T => fn term => Abs ("<eta_expand>", T, term))
+      (List.take (Ts, i))
+      (Term.list_comb (t', map Bound (i-1 downto 0)))
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
 (*               is the sum (over its constructors) of the product (over     *)

           val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
           val HOLogic_insert    =
             Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
         in
           (* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *)
-          map (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
+          map (fn ps => fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) ps
             HOLogic_empty_set) pairss
         end
       | Type (s, Ts) =>
         (case Datatype.get_info thy s of
           SOME info =>

                             "non-recursive codomain in recursive dtyp")
                         (* obtain interpretations for recursive arguments *)
                         (* interpretation list *)
                         val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs
                         (* apply 'intr' to all recursive arguments *)
-                        val result = List.foldl (fn (arg_i, i) =>
-                          interpretation_apply (i, arg_i)) intr arg_intrs
+                        val result = fold (fn arg_i => fn i =>
+                          interpretation_apply (i, arg_i)) arg_intrs intr
                         (* update 'REC_OPERATORS' *)
                         val _ = Array.update (arr, elem, (true, result))
                       in
                         result
                       end

           | intersection (_, _) =
           raise REFUTE ("lfp_interpreter",
             "intersection: interpretation for set is not a node")
         (* interpretation -> interpretaion *)
         fun lfp (Node resultsets) =
-          List.foldl (fn ((set, resultset), acc) =>
+          fold (fn (set, resultset) => fn acc =>
             if is_subset (resultset, set) then
               intersection (acc, set)
             else
-              acc) i_univ (i_sets ~~ resultsets)
+              acc) (i_sets ~~ resultsets) i_univ
           | lfp _ =
             raise REFUTE ("lfp_interpreter",
               "lfp: interpretation for function is not a node")
       in
         SOME (Node (map lfp i_funs), model, args)

           | union (_, _) =
           raise REFUTE ("gfp_interpreter",
             "union: interpretation for set is not a node")
         (* interpretation -> interpretaion *)
         fun gfp (Node resultsets) =
-          List.foldl (fn ((set, resultset), acc) =>
+          fold (fn (set, resultset) => fn acc =>
             if is_subset (set, resultset) then
               union (acc, set)
             else
-              acc) i_univ (i_sets ~~ resultsets)
+              acc) (i_sets ~~ resultsets) i_univ
           | gfp _ =
             raise REFUTE ("gfp_interpreter",
               "gfp: interpretation for function is not a node")
       in
         SOME (Node (map gfp i_funs), model, args)

         (* Term.term *)
         val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
         val HOLogic_insert    =
           Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
       in
-        SOME (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
-          HOLogic_empty_set pairs)
+        SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)
       end
     | Type ("prop", [])      =>
       (case index_from_interpretation intr of
         ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
       | 0  => SOME (HOLogic.mk_Trueprop HOLogic.true_const)