nth replaces List.nth
authorhaftmann
Mon Oct 12 10:24:08 2009 +0200 (2009-10-12)
changeset 329055e46c6704cee
parent 32904 9d27ebc82700
child 32906 ac97e8735cc2
nth replaces List.nth
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Oct 12 10:24:07 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Oct 12 10:24:08 2009 +0200
     1.3 @@ -65,8 +65,8 @@
     1.4          val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs)));
     1.5          val cert = cterm_of thy;
     1.6          val insts' = (map cert induct_Ps) ~~ (map cert insts);
     1.7 -        val induct' = refl RS ((List.nth
     1.8 -          (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
     1.9 +        val induct' = refl RS ((nth
    1.10 +          (split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
    1.11  
    1.12        in
    1.13          SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    1.14 @@ -130,10 +130,10 @@
    1.15            in (case (strip_dtyp dt, strip_type U) of
    1.16               ((_, DtRec m), (Us, _)) =>
    1.17                 let
    1.18 -                 val free2 = mk_Free "y" (Us ---> List.nth (rec_result_Ts, m)) k;
    1.19 +                 val free2 = mk_Free "y" (Us ---> nth rec_result_Ts m) k;
    1.20                   val i = length Us
    1.21                 in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
    1.22 -                     (map (pair "x") Us, List.nth (rec_sets', m) $
    1.23 +                     (map (pair "x") Us, nth rec_sets' m $
    1.24                         app_bnds free1 i $ app_bnds free2 i)) :: prems,
    1.25                     free1::t1s, free2::t2s)
    1.26                 end
    1.27 @@ -145,7 +145,7 @@
    1.28  
    1.29        in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
    1.30          (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
    1.31 -          list_comb (List.nth (rec_fns, l), t1s @ t2s)))], l + 1)
    1.32 +          list_comb (nth rec_fns l, t1s @ t2s)))], l + 1)
    1.33        end;
    1.34  
    1.35      val (rec_intr_ts, _) = Library.foldl (fn (x, ((d, T), set_name)) =>
    1.36 @@ -169,11 +169,11 @@
    1.37        let
    1.38          val distinct_tac =
    1.39            (if i < length newTs then
    1.40 -             full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1
    1.41 +             full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
    1.42             else full_simp_tac dist_ss 1);
    1.43  
    1.44          val inject = map (fn r => r RS iffD1)
    1.45 -          (if i < length newTs then List.nth (constr_inject, i)
    1.46 +          (if i < length newTs then nth constr_inject i
    1.47              else injects_of tname);
    1.48  
    1.49          fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =