# HG changeset patch
# User wenzelm
# Date 1255986176 -7200
# Node ID 715566791eb0ef2bfae2fe5cda3284c2c54a8306
# Parent  1c93cfa807bce06c25da04f13ea54761fb0a3375
always qualify NJ's old List.foldl/foldr in Isabelle/ML;

diff -r 1c93cfa807bc -r 715566791eb0 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -52,11 +52,11 @@
     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
     val rhs = hs
     val np = length ps
-    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
-      (foldr HOLogic.mk_imp c rhs, np) ps
+    val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
+      (List.foldr HOLogic.mk_imp c rhs, np) ps
     val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
       (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
-    val fm2 = foldr mk_all2 fm' vs
+    val fm2 = List.foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
 
 (*Object quantifier to meta --*)
diff -r 1c93cfa807bc -r 715566791eb0 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -58,11 +58,11 @@
       val rhs = hs
 (*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
     val np = length ps
-    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
-      (foldr HOLogic.mk_imp c rhs, np) ps
+    val (fm',np) =  List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
+      (List.foldr HOLogic.mk_imp c rhs, np) ps
     val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT)
       (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
-    val fm2 = foldr mk_all2 fm' vs
+    val fm2 = List.foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
 
 (*Object quantifier to meta --*)
diff -r 1c93cfa807bc -r 715566791eb0 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -73,11 +73,11 @@
       val rhs = hs
 (*    val (rhs,irhs) = List.partition (relevant (rev ps)) hs *)
     val np = length ps
-    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
-      (foldr HOLogic.mk_imp c rhs, np) ps
+    val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
+      (List.foldr HOLogic.mk_imp c rhs, np) ps
     val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
       (OldTerm.term_frees fm' @ OldTerm.term_vars fm');
-    val fm2 = foldr mk_all2 fm' vs
+    val fm2 = List.foldr mk_all2 fm' vs
   in (fm2, np + length vs, length rhs) end;
 
 (*Object quantifier to meta --*)
diff -r 1c93cfa807bc -r 715566791eb0 src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
--- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -9,7 +9,6 @@
   val pss_tree_to_cert : RealArith.pss_tree -> string
 
   val cert_to_pss_tree : Proof.context -> string -> RealArith.pss_tree
-
 end
 
 
@@ -101,7 +100,7 @@
   (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k)) 
 
 fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
-  foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.empty
+  List.foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.empty
 
 fun parse_cmonomial ctxt =
   rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
@@ -109,7 +108,7 @@
   rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
 
 fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
-  foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.empty
+  List.foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.empty
 
 (* positivstellensatz parser *)
 
diff -r 1c93cfa807bc -r 715566791eb0 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -252,7 +252,7 @@
       fun newName (Var(ix,_), (pairs,used)) = 
           let val v = Name.variant used (string_of_indexname ix)
           in  ((ix,v)::pairs, v::used)  end;
-      val (alist, _) = foldr newName ([], used) vars;
+      val (alist, _) = List.foldr newName ([], used) vars;
       fun mk_inst (Var(v,T)) = (Var(v,T),
            Free ((the o AList.lookup (op =) alist) v, T));
       val insts = map mk_inst vars;
diff -r 1c93cfa807bc -r 715566791eb0 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -897,7 +897,7 @@
 fun cprod ([], ys) = []
   | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
 
-fun cprods xss = foldr (map op :: o cprod) [[]] xss;
+fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
 
 fun cprods_subset [] = [[]]
   | cprods_subset (xs :: xss) =
diff -r 1c93cfa807bc -r 715566791eb0 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -825,7 +825,7 @@
 fun cprod ([], ys) = []
   | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
 
-fun cprods xss = foldr (map op :: o cprod) [[]] xss;
+fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
 
 
   
diff -r 1c93cfa807bc -r 715566791eb0 src/HOLCF/Tools/Domain/domain_syntax.ML
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -71,7 +71,7 @@
              to generate parse rules for non-alphanumeric names*)
         fun freetvar s n      = let val tvar = mk_TFree (s ^ string_of_int n) in
                                   if tvar mem typevars then freetvar ("t"^s) n else tvar end;
-        fun mk_matT (a,bs,c)  = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
+        fun mk_matT (a,bs,c)  = a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
         fun mat (con,args,mx) = (mat_name_ con,
                                  mk_matT(dtype, map third args, freetvar "t" 1),
                                  Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
diff -r 1c93cfa807bc -r 715566791eb0 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -36,7 +36,7 @@
 
 infixr 6 ->>; val (op ->>) = cfunT;
 
-fun cfunsT (Ts, U) = foldr cfunT U Ts;
+fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
 
 fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
   | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
diff -r 1c93cfa807bc -r 715566791eb0 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -18,6 +18,8 @@
 
 val forget_structure = PolyML.Compiler.forgetStructure;
 
+val _ = PolyML.Compiler.forgetValue "foldl";
+val _ = PolyML.Compiler.forgetValue "foldr";
 val _ = PolyML.Compiler.forgetValue "print";
 val _ = PolyML.Compiler.forgetValue "ref";
 val _ = PolyML.Compiler.forgetType "ref";
diff -r 1c93cfa807bc -r 715566791eb0 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/Tools/Metis/metis.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -64,6 +64,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* Isabelle ML SPECIFIC FUNCTIONS                                            *)
 (* ========================================================================= *)
@@ -348,6 +351,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* PP -- pretty-printing -- from the SML/NJ library                          *)
 (*                                                                           *)
@@ -1272,6 +1278,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* ML UTILITY FUNCTIONS                                                      *)
 (* Copyright (c) 2001-2004 Joe Hurd, distributed under the BSD License *)
@@ -1974,6 +1983,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* SUPPORT FOR LAZY EVALUATION                                               *)
 (* Copyright (c) 2007 Joe Hurd, distributed under the BSD License      *)
@@ -2053,6 +2065,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* ORDERED TYPES                                                             *)
 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
@@ -2189,6 +2204,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
@@ -2806,6 +2824,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* FINITE SETS                                                               *)
 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
@@ -3170,6 +3191,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
@@ -3803,6 +3827,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* FINITE MAPS                                                               *)
 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
@@ -4083,6 +4110,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* PRESERVING SHARING OF ML VALUES                                           *)
 (* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
@@ -4271,6 +4301,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML                                *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -4521,6 +4554,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* A HEAP DATATYPE FOR ML                                                    *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -4755,6 +4791,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* PARSER COMBINATORS                                                        *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -5258,6 +5297,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* PROCESSING COMMAND LINE OPTIONS                                           *)
 (* Copyright (c) 2003-2004 Joe Hurd, distributed under the BSD License *)
@@ -5527,6 +5569,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* NAMES                                                                     *)
 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
@@ -5802,6 +5847,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC TERMS                                                   *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -6578,6 +6626,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC SUBSTITUTIONS                                           *)
 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
@@ -6936,6 +6987,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC ATOMS                                                   *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -7373,6 +7427,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC FORMULAS                                                *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -8064,6 +8121,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC LITERALS                                                *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -8498,6 +8558,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* A LOGICAL KERNEL FOR FIRST ORDER CLAUSES                                  *)
 (* Copyright (c) 2001-2004 Joe Hurd, distributed under the BSD License *)
@@ -8787,6 +8850,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* PROOFS IN FIRST ORDER LOGIC                                               *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -9459,6 +9525,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS                     *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -10256,6 +10325,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* NORMALIZING FORMULAS                                                      *)
 (* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
@@ -11425,6 +11497,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* RANDOM FINITE MODELS                                                      *)
 (* Copyright (c) 2003-2007 Joe Hurd, distributed under the BSD License *)
@@ -12086,6 +12161,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES                             *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -12334,6 +12412,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS              *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -12813,6 +12894,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS              *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -12935,6 +13019,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS           *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -13073,6 +13160,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES                        *)
 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
@@ -13442,6 +13532,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* KNUTH-BENDIX TERM ORDERING CONSTRAINTS                                    *)
 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
@@ -13793,6 +13886,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* ORDERED REWRITING FOR FIRST ORDER TERMS                                   *)
 (* Copyright (c) 2003-2006 Joe Hurd, distributed under the BSD License *)
@@ -14507,6 +14603,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* A STORE FOR UNIT THEOREMS                                                 *)
 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
@@ -14731,6 +14830,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* CLAUSE = ID + THEOREM                                                     *)
 (* Copyright (c) 2002-2004 Joe Hurd, distributed under the BSD License *)
@@ -15145,6 +15247,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* THE ACTIVE SET OF CLAUSES                                                 *)
 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
@@ -16009,6 +16114,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* THE WAITING SET OF CLAUSES                                                *)
 (* Copyright (c) 2002-2007 Joe Hurd, distributed under the BSD License *)
@@ -16258,6 +16366,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* THE RESOLUTION PROOF PROCEDURE                                            *)
 (* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
@@ -16456,6 +16567,9 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
 (* ========================================================================= *)
 (* THE TPTP PROBLEM FILE FORMAT (TPTP v2)                                    *)
 (* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
diff -r 1c93cfa807bc -r 715566791eb0 src/Tools/Metis/metis_env.ML
--- a/src/Tools/Metis/metis_env.ML	Mon Oct 19 23:02:23 2009 +0200
+++ b/src/Tools/Metis/metis_env.ML	Mon Oct 19 23:02:56 2009 +0200
@@ -3,3 +3,6 @@
 val explode = String.explode;
 val implode = String.implode;
 val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+