Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 44058 ae85c5d64913
parent 43324 2b47822868e4
child 44121 44adaa6db327 
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -46,7 +46,7 @@
     val recTs = Datatype_Aux.get_rec_types descr' sorts;
     val newTs = take (length (hd descr)) recTs;
 
-    val {maxidx, ...} = rep_thm induct;
+    val maxidx = Thm.maxidx_of induct;
     val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
     fun prove_casedist_thm (i, (T, t)) =
isabelle