--- a/src/FOLP/simp.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/FOLP/simp.ML Thu Nov 28 10:44:24 1996 +0100
@@ -539,7 +539,7 @@
fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
let fun xn_list(x,n) =
let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
- in map eta_Var (ixs ~~ (take(n+1,Ts))) end
+ in ListPair.map eta_Var (ixs, take(n+1,Ts)) end
val lhs = list_comb(f,xn_list("X",k-1))
val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
--- a/src/Provers/simp.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/Provers/simp.ML Thu Nov 28 10:44:24 1996 +0100
@@ -565,7 +565,7 @@
fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
let fun xn_list(x,n) =
let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
- in map eta_Var (ixs ~~ (take(n+1,Ts))) end
+ in ListPair.map eta_Var (ixs, take(n+1,Ts)) end
val lhs = list_comb(f,xn_list("X",k-1))
val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
--- a/src/Provers/splitter.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/Provers/splitter.ML Thu Nov 28 10:44:24 1996 +0100
@@ -57,9 +57,9 @@
fun down [] t i = Bound 0
| down (p::ps) t i =
let val (h,ts) = strip_comb t
- val v1 = map var (take(p,ts) ~~ (i upto (i+p-1)))
+ val v1 = ListPair.map var (take(p,ts), i upto (i+p-1))
val u::us = drop(p,ts)
- val v2 = map var (us ~~ ((i+p) upto (i+length(ts)-2)))
+ val v2 = ListPair.map var (us, (i+p) upto (i+length(ts)-2))
in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;
in Abs("", T, down (rev pos) t maxi) end;
--- a/src/Pure/axclass.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/Pure/axclass.ML Thu Nov 28 10:44:24 1996 +0100
@@ -80,7 +80,7 @@
fun mk_arity (t, ss, c) =
let
val names = tl (variantlist (replicate (length ss + 1) "'", []));
- val tfrees = map TFree (names ~~ ss);
+ val tfrees = ListPair.map TFree (names, ss);
in
Logic.mk_inclass (Type (t, tfrees), c)
end;
--- a/src/Pure/drule.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/Pure/drule.ML Thu Nov 28 10:44:24 1996 +0100
@@ -339,7 +339,8 @@
val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars)
val inrs = add_term_tvars(prop,[]);
val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
- val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms')
+ val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
+ (inrs, nms')
val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
fun varpairs([],[]) = []
| varpairs((var as Var(v,T)) :: vars, b::bs) =
--- a/src/Pure/logic.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/Pure/logic.ML Thu Nov 28 10:44:24 1996 +0100
@@ -277,7 +277,8 @@
let val params = strip_params A;
val vars = if !auto_rename
then rename_vars (!rename_prefix, params)
- else variantlist(map #1 params,[]) ~~ map #2 params
+ else ListPair.zip (variantlist(map #1 params,[]),
+ map #2 params)
in list_all (vars, remove_params (length vars) n A)
end;
--- a/src/Pure/thm.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/Pure/thm.ML Thu Nov 28 10:44:24 1996 +0100
@@ -267,7 +267,7 @@
K None, K None,
[], true,
map (Sign.certify_typ sign) Ts,
- map read (bs~~Ts))
+ ListPair.map read (bs,Ts))
in map (cterm_of sign) us end
handle TYPE arg => error (Sign.exn_type_msg sign arg)
| TERM (msg, _) => error msg;
--- a/src/ZF/add_ind_def.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/ZF/add_ind_def.ML Thu Nov 28 10:44:24 1996 +0100
@@ -187,7 +187,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 **)
@@ -241,7 +241,8 @@
(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;
end;
--- a/src/ZF/ind_syntax.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/ZF/ind_syntax.ML Thu Nov 28 10:44:24 1996 +0100
@@ -97,7 +97,7 @@
mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm))
in map mk_intr constructs end;
-fun mk_all_intr_tms arg = flat (map mk_intr_tms (op ~~ arg));
+fun mk_all_intr_tms arg = List.concat (ListPair.map mk_intr_tms arg);
val Un = Const("op Un", [iT,iT]--->iT)
and empty = Const("0", iT)
--- a/src/ZF/indrule.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/ZF/indrule.ML Thu Nov 28 10:44:24 1996 +0100
@@ -143,7 +143,7 @@
(big_rec_tm,
Abs("z", Ind_Syntax.iT,
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_tprop(fold_bal (app Ind_Syntax.conj) qconcls);
--- a/src/ZF/intr_elim.ML Thu Nov 28 10:42:19 1996 +0100
+++ b/src/ZF/intr_elim.ML Thu Nov 28 10:44:24 1996 +0100
@@ -121,8 +121,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)));
(********)