--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Oct 20 20:54:31 2009 +0200
@@ -21,8 +21,8 @@
val rat_2 = Rat.two;
val rat_10 = Rat.rat_of_int 10;
val rat_1_2 = rat_1 // rat_2;
-val max = curry Int.max;
-val min = curry Int.min;
+val max = Integer.max;
+val min = Integer.min;
val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
val numerator_rat = Rat.quotient_of_rat #> fst #> Rat.rat_of_int;
--- a/src/HOL/SMT/Tools/z3_proof_terms.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_terms.ML Tue Oct 20 20:54:31 2009 +0200
@@ -89,7 +89,7 @@
local
fun mk_inst nctxt cert vs =
let
- val max = fold (curry Int.max o fst) vs 0
+ val max = fold (Integer.max o fst) vs 0
val names = fst (Name.variants (replicate (max + 1) var_prefix) nctxt)
fun mk (i, v) = (v, cert (Free (nth names i, #T (Thm.rep_cterm v))))
in map mk vs end
--- a/src/HOL/Tools/Function/scnp_solve.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML Tue Oct 20 20:54:31 2009 +0200
@@ -79,7 +79,7 @@
fun var_constrs (gp as GP (arities, gl)) =
let
val n = Int.max (num_graphs gp, num_prog_pts gp)
- val k = List.foldl Int.max 1 arities
+ val k = fold Integer.max arities 1
(* Injective, provided a < 8, x < n, and i < k. *)
fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Oct 20 20:54:31 2009 +0200
@@ -380,7 +380,7 @@
val pol' = augment pol
val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols'
val (l,cert) = grobner_weak vars' allpols
- val d = fold_rev (fold_rev (curry Int.max o hd o snd) o snd) cert 0
+ val d = fold (fold (Integer.max o hd o snd) o snd) cert 0
fun transform_monomial (c,m) =
grob_cmul (c,tl m) (grob_pow vars pol (d - hd m))
fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q []
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 20 20:54:31 2009 +0200
@@ -615,7 +615,7 @@
fun guess_nparams T =
let
val argTs = binder_types T
- val nparams = fold (curry Int.max)
+ val nparams = fold Integer.max
(map (fn x => x + 1) (find_indexes is_predT argTs)) 0
in nparams end;
--- a/src/HOL/Tools/prop_logic.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/Tools/prop_logic.ML Tue Oct 20 20:54:31 2009 +0200
@@ -387,7 +387,7 @@
if !next_idx_is_valid then
Unsynchronized.inc next_idx
else (
- next_idx := Termtab.fold (curry Int.max o snd) table 0;
+ next_idx := Termtab.fold (Integer.max o snd) table 0;
next_idx_is_valid := true;
Unsynchronized.inc next_idx
)
--- a/src/HOL/Tools/quickcheck_generators.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Oct 20 20:54:31 2009 +0200
@@ -256,7 +256,7 @@
val T = termifyT simpleT;
val tTs = (map o apsnd) termifyT simple_tTs;
val is_rec = exists is_some ks;
- val k = fold (fn NONE => I | SOME k => curry Int.max k) ks 0;
+ val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
val vs = Name.names Name.context "x" (map snd simple_tTs);
val vs' = (map o apsnd) termifyT vs;
val tc = HOLogic.mk_return T @{typ Random.seed}
--- a/src/HOL/Tools/record.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/Tools/record.ML Tue Oct 20 20:54:31 2009 +0200
@@ -750,7 +750,7 @@
val types = map snd flds';
val (args, rest) = splitargs (map fst flds') fargs;
val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
- val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) argtypes 0;
+ val midx = fold Term.maxidx_typ argtypes 0;
val varifyT = varifyT midx;
val vartypes = map varifyT types;
--- a/src/HOL/Tools/res_hol_clause.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Tue Oct 20 20:54:31 2009 +0200
@@ -437,7 +437,7 @@
case head of
CombConst (a,_,_) => (*predicate or function version of "equal"?*)
let val a = if a="equal" andalso not toplev then "c_fequal" else a
- val const_min_arity = Symtab.map_default (a,n) (curry Int.min n) const_min_arity
+ val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity
in
if toplev then (const_min_arity, const_needs_hBOOL)
else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
--- a/src/HOL/ex/predicate_compile.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Tue Oct 20 20:54:31 2009 +0200
@@ -542,7 +542,7 @@
fun guess_nparams T =
let
val argTs = binder_types T
- val nparams = fold (curry Int.max)
+ val nparams = fold Integer.max
(map (fn x => x + 1) (find_indexes is_predT argTs)) 0
in nparams end;
--- a/src/Provers/splitter.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/Provers/splitter.ML Tue Oct 20 20:54:31 2009 +0200
@@ -159,9 +159,9 @@
(* check if the innermost abstraction that needs to be removed
has a body of type T; otherwise the expansion thm will fail later on
*)
-fun type_test (T,lbnos,apsns) =
- let val (_,U: typ,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
- in T=U end;
+fun type_test (T, lbnos, apsns) =
+ let val (_, U: typ, _) = List.nth (apsns, foldl1 Int.min lbnos)
+ in T = U end;
(*************************************************************************
Create a "split_pack".
--- a/src/Pure/General/integer.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/Pure/General/integer.ML Tue Oct 20 20:54:31 2009 +0200
@@ -6,6 +6,8 @@
signature INTEGER =
sig
+ val min: int -> int -> int
+ val max: int -> int -> int
val add: int -> int -> int
val mult: int -> int -> int
val sum: int list -> int
@@ -23,6 +25,9 @@
structure Integer : INTEGER =
struct
+fun min x y = Int.min (x, y);
+fun max x y = Int.max (x, y);
+
fun add x y = x + y;
fun mult x y = x * y;
--- a/src/Pure/Tools/find_theorems.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue Oct 20 20:54:31 2009 +0200
@@ -109,7 +109,7 @@
in Vartab.fold (fn (_, (_, t)) => fn n => size_of_term t + n) subst 0 end;
fun bestmatch [] = NONE
- | bestmatch xs = SOME (foldr1 Int.min xs);
+ | bestmatch xs = SOME (foldl1 Int.min xs);
val match_thm = matches o refine_term;
in
@@ -142,7 +142,7 @@
(*dest rules always have assumptions, so a dest with one
assumption is as good as an intro rule with none*)
if not (null successful)
- then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
+ then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
end;
fun filter_intro doiff ctxt goal (_, thm) =
@@ -173,7 +173,7 @@
assumption is as good as an intro rule with none*)
if is_nontrivial (ProofContext.theory_of ctxt) (Thm.major_prem_of thm)
andalso not (null successful)
- then SOME (Thm.nprems_of thm - 1, foldr1 Int.min successful) else NONE
+ then SOME (Thm.nprems_of thm - 1, foldl1 Int.min successful) else NONE
end
else NONE
--- a/src/Pure/meta_simplifier.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/Pure/meta_simplifier.ML Tue Oct 20 20:54:31 2009 +0200
@@ -1158,8 +1158,8 @@
let
val prem' = Thm.rhs_of eqn;
val tprems = map term_of prems;
- val i = 1 + Library.foldl Int.max (~1, map (fn p =>
- find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
+ val i = 1 + fold Integer.max (map (fn p =>
+ find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
(rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
--- a/src/Tools/Code/code_thingol.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Oct 20 20:54:31 2009 +0200
@@ -420,7 +420,7 @@
fun same_arity thy thms =
let
val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
- val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
+ val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0;
in map (expand_eta thy k) thms end;
fun mk_desymbolization pre post mk vs =
--- a/src/Tools/atomize_elim.ML Tue Oct 20 20:03:23 2009 +0200
+++ b/src/Tools/atomize_elim.ML Tue Oct 20 20:54:31 2009 +0200
@@ -34,7 +34,7 @@
(* Compute inverse permutation *)
fun invert_perm pi =
- (pi @ ((0 upto (fold (curry Int.max) pi 0)) \\ pi))
+ (pi @ ((0 upto (fold Integer.max pi 0)) \\ pi))
|> map_index I
|> sort (int_ord o pairself snd)
|> map fst