Replaced map...~~ by ListPair.map
authorpaulson
Thu Nov 28 10:44:24 1996 +0100 (1996-11-28)
changeset 226682aef6857c5b
parent 2265 3123fef88dce
child 2267 b2326aefecbc
Replaced map...~~ by ListPair.map
src/FOLP/simp.ML
src/Provers/simp.ML
src/Provers/splitter.ML
src/Pure/axclass.ML
src/Pure/drule.ML
src/Pure/logic.ML
src/Pure/thm.ML
src/ZF/add_ind_def.ML
src/ZF/ind_syntax.ML
src/ZF/indrule.ML
src/ZF/intr_elim.ML
     1.1 --- a/src/FOLP/simp.ML	Thu Nov 28 10:42:19 1996 +0100
     1.2 +++ b/src/FOLP/simp.ML	Thu Nov 28 10:44:24 1996 +0100
     1.3 @@ -539,7 +539,7 @@
     1.4  fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
     1.5  let fun xn_list(x,n) =
     1.6          let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
     1.7 -        in map eta_Var (ixs ~~ (take(n+1,Ts))) end
     1.8 +        in ListPair.map eta_Var (ixs, take(n+1,Ts)) end
     1.9      val lhs = list_comb(f,xn_list("X",k-1))
    1.10      val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
    1.11  in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
     2.1 --- a/src/Provers/simp.ML	Thu Nov 28 10:42:19 1996 +0100
     2.2 +++ b/src/Provers/simp.ML	Thu Nov 28 10:44:24 1996 +0100
     2.3 @@ -565,7 +565,7 @@
     2.4  fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
     2.5  let fun xn_list(x,n) =
     2.6  	let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
     2.7 -	in map eta_Var (ixs ~~ (take(n+1,Ts))) end
     2.8 +	in ListPair.map eta_Var (ixs, take(n+1,Ts)) end
     2.9      val lhs = list_comb(f,xn_list("X",k-1))
    2.10      val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
    2.11  in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
     3.1 --- a/src/Provers/splitter.ML	Thu Nov 28 10:42:19 1996 +0100
     3.2 +++ b/src/Provers/splitter.ML	Thu Nov 28 10:44:24 1996 +0100
     3.3 @@ -57,9 +57,9 @@
     3.4        fun down [] t i = Bound 0
     3.5          | down (p::ps) t i =
     3.6              let val (h,ts) = strip_comb t
     3.7 -                val v1 = map var (take(p,ts) ~~ (i upto (i+p-1)))
     3.8 +                val v1 = ListPair.map var (take(p,ts), i upto (i+p-1))
     3.9                  val u::us = drop(p,ts)
    3.10 -                val v2 = map var (us ~~ ((i+p) upto (i+length(ts)-2)))
    3.11 +                val v2 = ListPair.map var (us, (i+p) upto (i+length(ts)-2))
    3.12        in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;
    3.13    in Abs("", T, down (rev pos) t maxi) end;
    3.14  
     4.1 --- a/src/Pure/axclass.ML	Thu Nov 28 10:42:19 1996 +0100
     4.2 +++ b/src/Pure/axclass.ML	Thu Nov 28 10:44:24 1996 +0100
     4.3 @@ -80,7 +80,7 @@
     4.4  fun mk_arity (t, ss, c) =
     4.5    let
     4.6      val names = tl (variantlist (replicate (length ss + 1) "'", []));
     4.7 -    val tfrees = map TFree (names ~~ ss);
     4.8 +    val tfrees = ListPair.map TFree (names, ss);
     4.9    in
    4.10      Logic.mk_inclass (Type (t, tfrees), c)
    4.11    end;
     5.1 --- a/src/Pure/drule.ML	Thu Nov 28 10:42:19 1996 +0100
     5.2 +++ b/src/Pure/drule.ML	Thu Nov 28 10:44:24 1996 +0100
     5.3 @@ -339,7 +339,8 @@
     5.4          val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars)
     5.5          val inrs = add_term_tvars(prop,[]);
     5.6          val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
     5.7 -        val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms')
     5.8 +        val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
     5.9 +	             (inrs, nms')
    5.10          val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
    5.11          fun varpairs([],[]) = []
    5.12            | varpairs((var as Var(v,T)) :: vars, b::bs) =
     6.1 --- a/src/Pure/logic.ML	Thu Nov 28 10:42:19 1996 +0100
     6.2 +++ b/src/Pure/logic.ML	Thu Nov 28 10:44:24 1996 +0100
     6.3 @@ -277,7 +277,8 @@
     6.4      let val params = strip_params A;
     6.5  	val vars = if !auto_rename 
     6.6  		   then rename_vars (!rename_prefix, params)
     6.7 -		   else variantlist(map #1 params,[]) ~~ map #2 params
     6.8 +		   else ListPair.zip (variantlist(map #1 params,[]),
     6.9 +				      map #2 params)
    6.10      in  list_all (vars, remove_params (length vars) n A)
    6.11      end;
    6.12  
     7.1 --- a/src/Pure/thm.ML	Thu Nov 28 10:42:19 1996 +0100
     7.2 +++ b/src/Pure/thm.ML	Thu Nov 28 10:44:24 1996 +0100
     7.3 @@ -267,7 +267,7 @@
     7.4  				  K None, K None, 
     7.5  				  [], true, 
     7.6  				  map (Sign.certify_typ sign) Ts, 
     7.7 -				  map read (bs~~Ts))
     7.8 +				  ListPair.map read (bs,Ts))
     7.9    in  map (cterm_of sign) us  end
    7.10    handle TYPE arg => error (Sign.exn_type_msg sign arg)
    7.11         | TERM (msg, _) => error msg;
     8.1 --- a/src/ZF/add_ind_def.ML	Thu Nov 28 10:42:19 1996 +0100
     8.2 +++ b/src/ZF/add_ind_def.ML	Thu Nov 28 10:44:24 1996 +0100
     8.3 @@ -187,7 +187,7 @@
     8.4                mk_defpair (list_comb (Const(name,T), args),
     8.5                            mk_inject npart kpart
     8.6                            (mk_inject ncon kcon (mk_tuple args)))
     8.7 -      in  map mk_def (con_ty_list ~~ (1 upto ncon))  end;
     8.8 +      in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
     8.9  
    8.10      (** Define the case operator **)
    8.11  
    8.12 @@ -241,7 +241,8 @@
    8.13          (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
    8.14  
    8.15      val axpairs =
    8.16 -        big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
    8.17 +        big_case_def :: flat (ListPair.map mk_con_defs
    8.18 +			      (1 upto npart, con_ty_lists))
    8.19  
    8.20      in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
    8.21  end;
     9.1 --- a/src/ZF/ind_syntax.ML	Thu Nov 28 10:42:19 1996 +0100
     9.2 +++ b/src/ZF/ind_syntax.ML	Thu Nov 28 10:44:24 1996 +0100
     9.3 @@ -97,7 +97,7 @@
     9.4                 mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 
     9.5    in  map mk_intr constructs  end;
     9.6  
     9.7 -fun mk_all_intr_tms arg = flat (map mk_intr_tms (op ~~ arg));
     9.8 +fun mk_all_intr_tms arg = List.concat (ListPair.map mk_intr_tms arg);
     9.9  
    9.10  val Un          = Const("op Un", [iT,iT]--->iT)
    9.11  and empty       = Const("0", iT)
    10.1 --- a/src/ZF/indrule.ML	Thu Nov 28 10:42:19 1996 +0100
    10.2 +++ b/src/ZF/indrule.ML	Thu Nov 28 10:44:24 1996 +0100
    10.3 @@ -143,7 +143,7 @@
    10.4         (big_rec_tm,
    10.5          Abs("z", Ind_Syntax.iT, 
    10.6              fold_bal (app Ind_Syntax.conj) 
    10.7 -            (map mk_rec_imp (Inductive.rec_tms~~preds)))))
    10.8 +            (ListPair.map mk_rec_imp (Inductive.rec_tms,preds)))))
    10.9  and mutual_induct_concl =
   10.10   Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls);
   10.11  
    11.1 --- a/src/ZF/intr_elim.ML	Thu Nov 28 10:42:19 1996 +0100
    11.2 +++ b/src/ZF/intr_elim.ML	Thu Nov 28 10:44:24 1996 +0100
    11.3 @@ -121,8 +121,8 @@
    11.4          and g rl = rl RS disjI2
    11.5      in  accesses_bal(f, g, asm_rl)  end;
    11.6  
    11.7 -val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
    11.8 -            (map (cterm_of sign) Inductive.intr_tms ~~ 
    11.9 +val intrs = ListPair.map (uncurry (prove_goalw_cterm part_rec_defs))
   11.10 +            (map (cterm_of sign) Inductive.intr_tms,
   11.11               map intro_tacsf (mk_disj_rls(length Inductive.intr_tms)));
   11.12  
   11.13  (********)