# HG changeset patch
# User paulson
# Date 849180693 -3600
# Node ID d7513875b2b89857dc72d67e74230db740033ffa
# Parent  820f68aec6ee15a922a8d947e925946b09d3feb6
Replaced map...~~ by ListPair.map

diff -r 820f68aec6ee -r d7513875b2b8 src/HOL/add_ind_def.ML
--- a/src/HOL/add_ind_def.ML	Thu Nov 28 12:28:52 1996 +0100
+++ b/src/HOL/add_ind_def.ML	Thu Nov 28 12:31:33 1996 +0100
@@ -118,8 +118,8 @@
           in  Part_const $ freeX $ Abs(w,domT,goodh)  end;
 
     (*Access to balanced disjoint sums via injections*)
-    val parts = map mk_Part
-                (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs) ~~
+    val parts = ListPair.map mk_Part
+                (accesses_bal (ap Inl, ap Inr, Bound 0) (length domTs),
                  domTs);
 
     (*replace each set by the corresponding Part(A,h)*)
@@ -186,7 +186,7 @@
               mk_defpair (list_comb (Const(name,T), args),
                           mk_inject npart kpart
                           (mk_inject ncon kcon (mk_tuple args)))
-*     in  map mk_def (con_ty_list ~~ (1 upto ncon))  end;
+*     in  ListPair.map mk_def (con_ty_list, (1 upto ncon))  end;
 
 *   (** Define the case operator **)
 
@@ -237,7 +237,7 @@
         (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
 
 *   val axpairs =
-        big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
+        big_case_def :: flat (ListPair.map mk_con_defs ((1 upto npart), con_ty_lists))
 
 *   in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
 ****************************************************************)
diff -r 820f68aec6ee -r d7513875b2b8 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Thu Nov 28 12:28:52 1996 +0100
+++ b/src/HOL/datatype.ML	Thu Nov 28 12:31:33 1996 +0100
@@ -54,7 +54,7 @@
 (* abstract rhs *)
 
 fun abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) =       
-  let val rargs = (map fst o 
+  let val rargs = (map #1 o 
                    (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc);
       val subs = map (fn (s,T) => (s,dummyT))
                    (rev(rename_wrt_term rhs rargs));
@@ -189,7 +189,7 @@
      (*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *)
       fun arg_eqs vns vns' =
         let fun mkeq(x,x') = x ^ "=" ^ x'
-        in space_implode " & " (map mkeq (vns~~vns')) end;
+        in space_implode " & " (ListPair.map mkeq (vns,vns')) end;
 
      (*Pretty printers for type lists;
        pp_typlist1: parentheses, pp_typlist2: brackets*)
@@ -310,7 +310,7 @@
         ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); 
 
 (* positions of the dtRek types in a list of dt_types, starting from 1  *)
-      fun rek_vars ts vns = map snd (filter (is_dtRek o fst) (ts ~~ vns))
+      fun rek_vars ts vns = map #2 (filter (is_dtRek o fst) (ts ~~ vns))
 
       fun rec_rule n (id,name,ts,vns,_) = 
         let val args = opt_parens(space_implode ") (" vns)
@@ -365,7 +365,7 @@
 
       fun Ci_neg2() =
         let val ord_t = tname ^ "_ord";
-          val cis = cons_list ~~ (0 upto (num_of_cons - 1))
+          val cis = ListPair.zip (cons_list, 0 upto (num_of_cons - 1))
           fun Ci_neg2equals ((id, name, _, vns, _), n) =
             let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n)
             in (ord_t ^ "_" ^ id, ax) end
diff -r 820f68aec6ee -r d7513875b2b8 src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Thu Nov 28 12:28:52 1996 +0100
+++ b/src/HOL/indrule.ML	Thu Nov 28 12:31:33 1996 +0100
@@ -143,7 +143,7 @@
        (big_rec_tm,
         Abs("z", elem_type, 
             fold_bal (app Ind_Syntax.conj) 
-            (map mk_rec_imp (Inductive.rec_tms~~preds)))))
+            (ListPair.map mk_rec_imp (Inductive.rec_tms,preds)))))
 and mutual_induct_concl = 
     Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls);
 
diff -r 820f68aec6ee -r d7513875b2b8 src/HOL/intr_elim.ML
--- a/src/HOL/intr_elim.ML	Thu Nov 28 12:28:52 1996 +0100
+++ b/src/HOL/intr_elim.ML	Thu Nov 28 12:31:33 1996 +0100
@@ -100,8 +100,8 @@
         and g rl = rl RS disjI2
     in  accesses_bal(f, g, asm_rl)  end;
 
-val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
-            (map (cterm_of sign) Inductive.intr_tms ~~ 
+val intrs = ListPair.map (uncurry (prove_goalw_cterm part_rec_defs))
+            (map (cterm_of sign) Inductive.intr_tms,
              map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
 
 (********)