--- 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 --*)
--- 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 --*)
--- 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 --*)
--- 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 *)
--- 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;
--- 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) =
--- 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;
--- 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));
--- 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], []);
--- 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";
--- 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 *)
--- 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;
+