--- 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;
****************************************************************)
--- 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
--- 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);
--- 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)));
(********)