# HG changeset patch
# User haftmann
# Date 1133507219 -3600
# Node ID 444f16d232a2200be135b3712e67745a4f55fb50
# Parent  221d47d17a81908414b3ddf2700bd24491cc2a5d
introduced new map2, fold

diff -r 221d47d17a81 -r 444f16d232a2 src/HOL/Tools/datatype_rep_proofs.ML
--- 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');
 
diff -r 221d47d17a81 -r 444f16d232a2 src/HOL/Tools/inductive_package.ML
--- 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;
diff -r 221d47d17a81 -r 444f16d232a2 src/HOL/Tools/record_package.ML
--- 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
diff -r 221d47d17a81 -r 444f16d232a2 src/Provers/Arith/fast_lin_arith.ML
--- 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))
diff -r 221d47d17a81 -r 444f16d232a2 src/Provers/induct_method.ML
--- 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
diff -r 221d47d17a81 -r 444f16d232a2 src/Pure/IsaPlanner/isand.ML
--- 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 
diff -r 221d47d17a81 -r 444f16d232a2 src/Pure/Isar/locale.ML
--- 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);
diff -r 221d47d17a81 -r 444f16d232a2 src/Pure/Tools/class_package.ML
--- 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
diff -r 221d47d17a81 -r 444f16d232a2 src/Pure/Tools/codegen_package.ML
--- 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
diff -r 221d47d17a81 -r 444f16d232a2 src/Pure/Tools/codegen_thingol.ML
--- 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
diff -r 221d47d17a81 -r 444f16d232a2 src/Pure/library.ML
--- 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 *)