author boehmes Tue, 20 Oct 2009 14:22:54 +0200 changeset 33018 49abb2ae1379 parent 33017 4fb8a33f74d6 (current diff) parent 33015 575bd6548df9 (diff) child 33020 0908ed080ccf
merged
--- a/doc-src/TutorialI/Rules/rules.tex	Tue Oct 20 14:22:02 2009 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Tue Oct 20 14:22:54 2009 +0200
@@ -1357,7 +1357,7 @@
some $x$ such that $P(x)$ is true, provided one exists.
Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.

-Here is the definition of~\cdx{inv}, which expresses inverses of
+Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_onto}, which we ignore here.} which expresses inverses of
functions:
\begin{isabelle}
inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Oct 20 14:22:54 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 Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Oct 20 14:22:54 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 Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Oct 20 14:22:54 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/Hilbert_Choice.thy Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Hilbert_Choice.thy Tue Oct 20 14:22:54 2009 +0200 @@ -91,6 +91,9 @@ subsection {*Function Inverse*} +lemma inv_def: "inv f = (%y. SOME x. f x = y)" +by(simp add: inv_onto_def) + lemma inv_onto_into: "x : f  A ==> inv_onto A f x : A" apply (simp add: inv_onto_def) apply (fast intro: someI2) --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Tue Oct 20 14:22:54 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/Library/Sum_Of_Squares/sum_of_squares.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Oct 20 14:22:54 2009 +0200 @@ -223,7 +223,7 @@ fun monomial_var x = FuncUtil.Ctermfunc.onefunc (x, 1); val monomial_mul = - FuncUtil.Ctermfunc.combine (curry op +) (K false); + FuncUtil.Ctermfunc.combine Integer.add (K false); fun monomial_pow m k = if k = 0 then monomial_1 @@ -233,7 +233,7 @@ FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => FuncUtil.Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;; fun monomial_div m1 m2 = - let val m = FuncUtil.Ctermfunc.combine (curry op +) + let val m = FuncUtil.Ctermfunc.combine Integer.add (fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn x => ~ x) m2) in if FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m else error "monomial_div: non-divisible" --- a/src/HOL/Library/positivstellensatz.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Tue Oct 20 14:22:54 2009 +0200 @@ -83,8 +83,8 @@ else let val mon1 = dest_monomial m1 val mon2 = dest_monomial m2 - val deg1 = fold (curry op + o snd) mon1 0 - val deg2 = fold (curry op + o snd) mon2 0 + val deg1 = fold (Integer.add o snd) mon1 0 + val deg2 = fold (Integer.add o snd) mon2 0 in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2) end; --- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Oct 20 14:22:54 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/SMT/etc/settings Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/SMT/etc/settings Tue Oct 20 14:22:54 2009 +0200 @@ -1,10 +1,10 @@ ISABELLE_SMT="$COMPONENT"

-REMOTE_SMT_SOLVER="$COMPONENT/lib/scripts/remote_smt.pl" +REMOTE_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/remote_smt.pl"

REMOTE_SMT_URL="http://www4.in.tum.de/smt/smt"

-CERT_SMT_SOLVER="$COMPONENT/lib/scripts/cert_smt.pl" +CERT_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/cert_smt.pl"

#
# Paths to local SMT solvers:
--- a/src/HOL/Statespace/state_fun.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -157,8 +157,6 @@
| _ => NONE ));

-fun foldl1 f (x::xs) = foldl f x xs;
-
local
val meta_ext = @{thm StateFun.meta_ext};
@@ -182,7 +180,7 @@
in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end

fun mk_comps fs =
-                   foldl1 (fn ((f,fT),(g,gT)) => mk_comp f fT g gT) fs;
+                   foldl1 (fn ((f,fT),(g,gT)) => mk_comp g gT f fT) fs;

fun append n c cT f fT d dT comps =
(case AList.lookup (op aconv) comps n of
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -20,7 +20,7 @@
val (_, _, constrs) = the (AList.lookup (op =) descr i);
fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
then NONE
-          else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
+          else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
| arg_nonempty _ = SOME 0;
fun max xs = Library.foldl
(fn (NONE, _) => NONE
--- a/src/HOL/Tools/Function/fundef_datatype.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -54,7 +54,7 @@
val _ = map check_constr_pattern args

(* just count occurrences to check linearity *)
-      val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 > length qs
+      val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs
then err "Nonlinear patterns" else ()
in
()
--- a/src/HOL/Tools/Function/scnp_solve.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -46,7 +46,7 @@
fun num_prog_pts (GP (arities, _)) = length arities ;
fun num_graphs (GP (_, gs)) = length gs ;
fun arity (GP (arities, gl)) i = nth arities i ;
-fun ndigits (GP (arities, _)) = IntInf.log2 (List.foldl (op +) 0 arities) + 1
+fun ndigits (GP (arities, _)) = IntInf.log2 (Integer.sum arities) + 1

(** Propositional formulas **)
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -391,8 +391,8 @@
in fn tm1 => fn tm2 =>
let val vdegs1 = map dest_varpow (powervars tm1)
val vdegs2 = map dest_varpow (powervars tm2)
-      val deg1 = fold_rev ((curry (op +)) o snd) vdegs1 num_0
-      val deg2 = fold_rev ((curry (op +)) o snd) vdegs2 num_0
+      val deg1 = fold (Integer.add o snd) vdegs1 num_0
+      val deg2 = fold (Integer.add o snd) vdegs2 num_0
in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1
else lexorder vdegs1 vdegs2
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 20 14:22:54 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/Tools/Qelim/cooper.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -188,7 +188,7 @@
(Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times}, _)$ c1 $x1)$ r1,
Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times}, _)$ c2 $x2)$ r2) =>
if x1 = x2 then
-     let val c = numeral2 (curry op +) c1 c2
+     let val c = numeral2 Integer.add c1 c2
in if c = zero then linear_add vars r1 r2
else addC$(mulC$c$x1)$(linear_add vars r1 r2)
end
@@ -198,7 +198,7 @@
addC $(mulC$ c1 $x1)$ linear_add vars r1 tm2
| (_, Const (@{const_name HOL.plus}, _) $(Const (@{const_name HOL.times}, _)$ c2 $x2)$ r2) =>
addC $(mulC$ c2 $x2)$ linear_add vars tm1 r2
- | (_, _) => numeral2 (curry op +) tm1 tm2;
+ | (_, _) => numeral2 Integer.add tm1 tm2;

fun linear_neg tm = linear_cmul ~1 tm;
fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
--- a/src/HOL/Tools/refute.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -1616,30 +1616,14 @@
end;

(* ------------------------------------------------------------------------- *)
-(* sum: returns the sum of a list 'xs' of integers                           *)
-(* ------------------------------------------------------------------------- *)
-
-  (* int list -> int *)
-
-  fun sum xs = List.foldl op+ 0 xs;
-
-(* ------------------------------------------------------------------------- *)
-(* product: returns the product of a list 'xs' of integers                   *)
-(* ------------------------------------------------------------------------- *)
-
-  (* int list -> int *)
-
-  fun product xs = List.foldl op* 1 xs;
-
-(* ------------------------------------------------------------------------- *)
(* size_of_dtyp: the size of (an initial fragment of) an inductive data type *)
(*               is the sum (over its constructors) of the product (over     *)
(*               their arguments) of the size of the argument types          *)
(* ------------------------------------------------------------------------- *)

fun size_of_dtyp thy typ_sizes descr typ_assoc constructors =
-    sum (map (fn (_, dtyps) =>
-      product (map (size_of_type thy (typ_sizes, []) o
+    Integer.sum (map (fn (_, dtyps) =>
+      Integer.prod (map (size_of_type thy (typ_sizes, []) o
(typ_of_dtyp descr typ_assoc)) dtyps))
constructors);

@@ -2326,8 +2310,8 @@
let
(* number of all constructors, including those of different  *)
(* (mutually recursive) datatypes within the same descriptor *)
-              val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs)
-                (#descr info))
+              val mconstrs_count =
+                Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info))
in
if mconstrs_count < length params then
(* too many actual parameters; for now we'll use the *)
--- a/src/HOL/ex/predicate_compile.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Oct 20 14:22:54 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	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Oct 20 14:22:54 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	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/HOLCF/Tools/fixrec.ML	Tue Oct 20 14:22:54 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/Provers/Arith/fast_lin_arith.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -301,14 +301,14 @@
if n = 1 then i
else if n = 0 andalso ty = Lt then sys_error "multiply_ineq"
else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq"
-  else Lineq (n * k, ty, map (curry op* n) l, Multiplied (n, just));
+  else Lineq (n * k, ty, map (Integer.mult n) l, Multiplied (n, just));

(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)

fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
-  let val l = map2 (curry (op +)) l1 l2
+  let val l = map2 Integer.add l1 l2

(* ------------------------------------------------------------------------- *)
--- a/src/Pure/General/integer.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/Pure/General/integer.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -1,13 +1,16 @@
(*  Title:      Pure/General/integer.ML
Author:     Florian Haftmann, TU Muenchen

-Unbounded integers.
+Auxiliary operations on (unbounded) integers.
*)

signature INTEGER =
sig
+  val add: int -> int -> int
+  val mult: int -> int -> int
+  val sum: int list -> int
+  val prod: int list -> int
val sign: int -> order
-  val sum: int list -> int
val div_mod: int -> int -> int * int
val square: int -> int
val pow: int -> int -> int (* exponent -> base -> result *)
@@ -20,9 +23,13 @@
structure Integer : INTEGER =
struct

-fun sign x = int_ord (x, 0);
+fun add x y = x + y;
+fun mult x y = x * y;

-fun sum xs = fold (curry op +) xs 0;
+fun sum xs = fold add xs 0;
+fun prod xs = fold mult xs 1;
+
+fun sign x = int_ord (x, 0);

fun div_mod x y = IntInf.divMod (x, y);

--- a/src/Pure/ML-Systems/polyml_common.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Oct 20 14:22:54 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	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/Tools/Metis/metis.ML	Tue Oct 20 14:22:54 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                                                      *)
@@ -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                                               *)
@@ -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                                                             *)
@@ -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                      *)
@@ -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                                                               *)
@@ -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                      *)
@@ -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                                                               *)
@@ -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                                           *)
@@ -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                                *)
@@ -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                                                    *)
@@ -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                                                        *)
@@ -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                                           *)
@@ -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                                                                     *)
@@ -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                                                   *)
@@ -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                                           *)
@@ -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                                                   *)
@@ -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                                                *)
@@ -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                                                *)
@@ -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                                  *)
@@ -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                                               *)
@@ -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                     *)
@@ -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                                                      *)
@@ -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                                                      *)
@@ -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                             *)
@@ -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              *)
@@ -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              *)
@@ -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           *)
@@ -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                        *)
@@ -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                                    *)
@@ -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                                   *)
@@ -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                                                 *)
@@ -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                                                     *)
@@ -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                                                 *)
@@ -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                                                *)
@@ -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                                            *)
@@ -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	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/Tools/Metis/metis_env.ML	Tue Oct 20 14:22:54 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;
+
--- a/src/Tools/atomize_elim.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/Tools/atomize_elim.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -42,7 +42,7 @@
(* rearrange_prems as a conversion *)
fun rearrange_prems_conv pi ct =
let
-      val pi' = 0 :: map (curry op + 1) pi
+      val pi' = 0 :: map (Integer.add 1) pi
val fwd  = Thm.trivial ct
|> Drule.rearrange_prems pi'
val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))
--- a/src/Tools/nbe.ML	Tue Oct 20 14:22:02 2009 +0200
+++ b/src/Tools/nbe.ML	Tue Oct 20 14:22:54 2009 +0200
@@ -303,7 +303,7 @@
fun subst_nonlin_vars args =
let
val vs = (fold o Code_Thingol.fold_varnames)
-          (fn v => AList.map_default (op =) (v, 0) (curry (op +) 1)) args [];
+          (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args [];
val names = Name.make_context (map fst vs);
fun declare v k ctxt = let val vs = Name.invents ctxt v k
in (vs, fold Name.declare vs ctxt) end;`