src/HOL/Tools/TFL/casesplit.ML

--- a/src/HOL/Tools/TFL/casesplit.ML	Wed Nov 30 21:14:01 2011 +0100
+++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Nov 30 23:30:08 2011 +0100
@@ -36,9 +36,9 @@
                      Type(ty_str, _) => ty_str
                    | TFree(s,_)  => error ("Free type: " ^ s)
                    | TVar((s,i),_) => error ("Free variable: " ^ s)
-      val dt = Datatype.the_info thy ty_str
+      val {induct, ...} = Datatype.the_info thy ty_str
     in
-      cases_thm_of_induct_thm (#induct dt)
+      cases_thm_of_induct_thm induct
     end;