src/HOL/Tools/TFL/casesplit.ML

--- a/src/HOL/Tools/TFL/casesplit.ML	Fri Sep 25 10:20:03 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Sun Sep 27 09:52:23 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 (#induction dt)
+      cases_thm_of_induct_thm (snd (#inducts dt))
     end;
 
 (*