# HG changeset patch # User paulson # Date 849174264 -3600 # Node ID 82aef6857c5b5d7a797df385a1002947bd0e9ffe # Parent 3123fef88dce17e91ce873a03a9ed1963aefcd97 Replaced map...~~ by ListPair.map diff -r 3123fef88dce -r 82aef6857c5b src/FOLP/simp.ML --- 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; diff -r 3123fef88dce -r 82aef6857c5b src/Provers/simp.ML --- 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; diff -r 3123fef88dce -r 82aef6857c5b src/Provers/splitter.ML --- 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; diff -r 3123fef88dce -r 82aef6857c5b src/Pure/axclass.ML --- 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; diff -r 3123fef88dce -r 82aef6857c5b src/Pure/drule.ML --- 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) = diff -r 3123fef88dce -r 82aef6857c5b src/Pure/logic.ML --- 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; diff -r 3123fef88dce -r 82aef6857c5b src/Pure/thm.ML --- 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; diff -r 3123fef88dce -r 82aef6857c5b src/ZF/add_ind_def.ML --- 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; diff -r 3123fef88dce -r 82aef6857c5b src/ZF/ind_syntax.ML --- 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) diff -r 3123fef88dce -r 82aef6857c5b src/ZF/indrule.ML --- 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); diff -r 3123fef88dce -r 82aef6857c5b src/ZF/intr_elim.ML --- 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))); (********)