src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 44058 ae85c5d64913
parent 43324 2b47822868e4
child 44121 44adaa6db327
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 08 16:38:59 2011 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 08 17:23:15 2011 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4      val recTs = Datatype_Aux.get_rec_types descr' sorts;
     1.5      val newTs = take (length (hd descr)) recTs;
     1.6  
     1.7 -    val {maxidx, ...} = rep_thm induct;
     1.8 +    val maxidx = Thm.maxidx_of induct;
     1.9      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.10  
    1.11      fun prove_casedist_thm (i, (T, t)) =