src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33063 4d462963a7db
parent 33056 791a4655cae3
child 33171 292970b42770
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 22 10:52:07 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 22 13:48:06 2009 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4      val {maxidx, ...} = rep_thm induct;
     1.5      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
     1.6  
     1.7 -    fun prove_casedist_thm ((i, t), T) =
     1.8 +    fun prove_casedist_thm (i, (T, t)) =
     1.9        let
    1.10          val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
    1.11            Abs ("z", T', Const ("True", T''))) induct_Ps;
    1.12 @@ -77,8 +77,8 @@
    1.13               REPEAT (rtac TrueI 1)])
    1.14        end;
    1.15  
    1.16 -    val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
    1.17 -      (DatatypeProp.make_casedists descr sorts) ~~ newTs)
    1.18 +    val casedist_thms = map_index prove_casedist_thm
    1.19 +      (newTs ~~ DatatypeProp.make_casedists descr sorts)
    1.20    in
    1.21      thy
    1.22      |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms