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/TFL/casesplit.ML
changeset 32727 9072201cd69d
parent 32712 ec5976f4d3d8
child 32952 aeb1e44fbc19 
--- a/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -96,7 +96,7 @@
                    | TVar((s,i),_) => error ("Free variable: " ^ s)
       val dt = Datatype.the_info thy ty_str
     in
-      cases_thm_of_induct_thm (snd (#inducts dt))
+      cases_thm_of_induct_thm (#induct dt)
     end;
 
 (*
isabelle