src/HOL/Tools/TFL/casesplit.ML

--- a/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 01 19:28:00 2014 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 01 19:57:48 2014 +0200
@@ -24,7 +24,7 @@
                      Type(ty_str, _) => ty_str
                    | TFree(s,_)  => error ("Free type: " ^ s)
                    | TVar((s,i),_) => error ("Free variable: " ^ s)
-      val {induct, ...} = Old_Datatype_Data.the_info thy ty_str
+      val {induct, ...} = BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Keep_Nesting ty_str
     in
       cases_thm_of_induct_thm induct
     end;