--- 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};
val ss' = (HOL_ss addsimps
@@ -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));
(* ------------------------------------------------------------------------- *)
(* Add together (in)equations. *)
(* ------------------------------------------------------------------------- *)
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
in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end;
(* ------------------------------------------------------------------------- *)
--- 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 *)
(* 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 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;