--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Dec 02 08:06:59 2005 +0100
@@ -505,8 +505,8 @@
val Abs_inverse_thms' =
map #1 newT_iso_axms @
- map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp])
- (iso_inj_thms_unfolded, iso_thms);
+ map2 (fn r_inj => fn r => f_myinv_f OF [r_inj, r RS mp])
+ iso_inj_thms_unfolded iso_thms;
val Abs_inverse_thms = List.concat (map mk_funs_inv Abs_inverse_thms');
--- a/src/HOL/Tools/inductive_package.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/HOL/Tools/inductive_package.ML Fri Dec 02 08:06:59 2005 +0100
@@ -448,12 +448,12 @@
fun add_cases_induct no_elim no_induct coind names elims induct =
let
- fun cases_spec (name, elim) thy =
+ fun cases_spec name elim thy =
thy
|> Theory.add_path (Sign.base_name name)
|> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
|> Theory.parent_path;
- val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
+ val cases_specs = if no_elim then [] else map2 cases_spec names elims;
val induct_att =
if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global;
--- a/src/HOL/Tools/record_package.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/HOL/Tools/record_package.ML Fri Dec 02 08:06:59 2005 +0100
@@ -1745,7 +1745,7 @@
|> Theory.add_tyabbrs_i recordT_specs
|> Theory.add_path bname
|> Theory.add_consts_i
- (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
+ (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
|> (Theory.add_consts_i o map Syntax.no_syn)
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
|> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Dec 02 08:06:59 2005 +0100
@@ -279,7 +279,7 @@
(* ------------------------------------------------------------------------- *)
fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
- let val l = map2 (op +) (l1,l2)
+ let val l = map2 (curry (op +)) l1 l2
in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end;
(* ------------------------------------------------------------------------- *)
@@ -504,7 +504,7 @@
let val (m,(lhs,i,rel,rhs,j,discrete)) = integ item
val lhsa = map (coeff lhs) atoms
and rhsa = map (coeff rhs) atoms
- val diff = map2 (op -) (rhsa,lhsa)
+ val diff = map2 (curry (op -)) rhsa lhsa
val c = i-j
val just = Asm k
fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j))
--- a/src/Provers/induct_method.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/Provers/induct_method.ML Fri Dec 02 08:06:59 2005 +0100
@@ -298,7 +298,7 @@
val certT = Thm.ctyp_of thy;
val pairs = Envir.alist_of env;
val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
- val xs = map2 (cert o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts);
+ val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
in
--- a/src/Pure/IsaPlanner/isand.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/Pure/IsaPlanner/isand.ML Fri Dec 02 08:06:59 2005 +0100
@@ -635,7 +635,7 @@
val (subgoals, expf) = subgoal_thms th;
(* fun export_sg (th, exp) = exp th; *)
fun export_sgs expfs solthms =
- expf (map2 (op |>) (solthms, expfs));
+ expf (map2 (curry (op |>)) solthms expfs);
(* expf (map export_sg (ths ~~ expfs)); *)
in
apsnd export_sgs (Library.split_list (map (apsnd export_solution o
--- a/src/Pure/Isar/locale.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/Pure/Isar/locale.ML Fri Dec 02 08:06:59 2005 +0100
@@ -1219,8 +1219,8 @@
(* CB: resolve schematic variables (patterns) in conclusion and external
elements. *)
- val all_propp' = map2 (op ~~)
- (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
+ val all_propp' = map2 (curry (op ~~))
+ (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
val (concl, propp) = splitAt(length raw_concl, all_propp');
val propps = unflat raw_propps propp;
val proppss = map (uncurry unflat) (raw_proppss ~~ propps);
--- a/src/Pure/Tools/class_package.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/Pure/Tools/class_package.ML Fri Dec 02 08:06:59 2005 +0100
@@ -186,7 +186,7 @@
val vars_used = fold (fn ty => curry (gen_union (op =))
(map fst (typ_tfrees ty) |> remove (op =) "'a")) const_signs [];
val vars_new = Term.invent_names vars_used "'a" (length arities);
- val typ_arity = Type (tyco, map2 TFree (vars_new, arities));
+ val typ_arity = Type (tyco, map2 (curry TFree) vars_new arities);
val instmem_signs =
map (typ_subst_atomic [(TFree ("'a", []), typ_arity)]) const_signs;
in consts ~~ instmem_signs end;
@@ -225,8 +225,8 @@
of (subclass::deriv) => (rev deriv, find_index_eq subclass subclasses);
fun mk_lookup (sort_def, (Type (tycon, tys))) =
let
- val arity_lookup = map2 mk_lookup
- (map (filter_class thy) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def), tys)
+ val arity_lookup = map2 (curry mk_lookup)
+ (map (filter_class thy) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def)) tys
in map (fn class => Instance ((class, tycon), arity_lookup)) sort_def end
| mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
let
--- a/src/Pure/Tools/codegen_package.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML Fri Dec 02 08:06:59 2005 +0100
@@ -827,7 +827,7 @@
let
val vs = gen_names i;
val tys = Library.take (i, (fst o strip_type) ty);
- val frees = map2 Free (vs, tys);
+ val frees = map2 (curry Free) vs tys;
val t' = Envir.beta_norm (list_comb (t, frees));
in
trns
--- a/src/Pure/Tools/codegen_thingol.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Fri Dec 02 08:06:59 2005 +0100
@@ -1109,7 +1109,7 @@
|> Term.invent_names ((vars_of_iexprs o map snd) ds @ (vars_of_ipats o Library.flat o map fst) ds) "d"
|> unflat (map snd sortctxt);
val _ = writeln ("class 2");
- val vname_alist = map2 (fn ((vt, sort), vs) => (vt, vs ~~ sort)) (sortctxt, varnames_ctxt);
+ val vname_alist = map2 (fn (vt, sort) => fn vs => (vt, vs ~~ sort)) sortctxt varnames_ctxt;
val _ = writeln ("class 3");
fun add_typarms ty =
map (foldr1 (op xx) o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist
--- a/src/Pure/library.ML Thu Dec 01 22:43:15 2005 +0100
+++ b/src/Pure/library.ML Fri Dec 02 08:06:59 2005 +0100
@@ -97,7 +97,6 @@
val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
- val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
@@ -113,18 +112,16 @@
val find_index_eq: ''a -> ''a list -> int
val find_first: ('a -> bool) -> 'a list -> 'a option
val get_first: ('a -> 'b option) -> 'a list -> 'b option
+ val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+ val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
+ val ~~ : 'a list * 'b list -> ('a * 'b) list
+ val split_list: ('a * 'b) list -> 'a list * 'b list
val separate: 'a -> 'a list -> 'a list
val replicate: int -> 'a -> 'a list
val multiply: 'a list -> 'a list list -> 'a list list
val product: 'a list -> 'b list -> ('a * 'b) list
val filter: ('a -> bool) -> 'a list -> 'a list
val filter_out: ('a -> bool) -> 'a list -> 'a list
- val map2: ('a * 'b -> 'c) -> 'a list * 'b list -> 'c list
- val exists2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
- val forall2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
- val seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit
- val ~~ : 'a list * 'b list -> ('a * 'b) list
- val split_list: ('a * 'b) list -> 'a list * 'b list
val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val prefix: ''a list * ''a list -> bool
val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
@@ -467,13 +464,6 @@
| fold_aux (x :: xs) y = fold_aux xs (f x y);
in fold_aux end;
-fun fold2 f =
- let
- fun fold_aux [] [] z = z
- | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
- | fold_aux _ _ _ = raise UnequalLengths;
- in fold_aux end;
-
fun fold_rev f =
let
fun fold_aux [] y = y
@@ -643,21 +633,17 @@
exception UnequalLengths;
-fun map2 _ ([], []) = []
- | map2 f (x :: xs, y :: ys) = f (x, y) :: map2 f (xs, ys)
- | map2 _ _ = raise UnequalLengths;
-
-fun exists2 _ ([], []) = false
- | exists2 pred (x :: xs, y :: ys) = pred (x, y) orelse exists2 pred (xs, ys)
- | exists2 _ _ = raise UnequalLengths;
+fun map2 _ [] [] = []
+ | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
+ | map2 _ _ _ = raise UnequalLengths;
-fun forall2 _ ([], []) = true
- | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys)
- | forall2 _ _ = raise UnequalLengths;
+fun fold2 f =
+ let
+ fun fold_aux [] [] z = z
+ | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
+ | fold_aux _ _ _ = raise UnequalLengths;
+ in fold_aux end;
-fun seq2 _ ([], []) = ()
- | seq2 f (x :: xs, y :: ys) = (f (x, y); seq2 f (xs, ys))
- | seq2 _ _ = raise UnequalLengths;
(*combine two lists forming a list of pairs:
[x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*)
@@ -669,7 +655,11 @@
[(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*)
val split_list = ListPair.unzip;
-fun equal_lists eq (xs, ys) = length xs = length ys andalso forall2 eq (xs, ys);
+fun equal_lists eq (xs, ys) =
+ let
+ fun eq' [] [] = true
+ | eq' (x :: xs) (y :: ys) = eq (x, y) andalso eq' xs ys
+ in length xs = length ys andalso eq' xs ys end;
(* prefixes, suffixes *)