src/HOL/Tools/TFL/tfl.ML

--- a/src/HOL/Tools/TFL/tfl.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -435,7 +435,7 @@
        put_simpset HOL_basic_ss ctxt
           addsimps case_rewrites
           |> fold (Simplifier.add_cong o #case_cong_weak o snd)
-              (Symtab.dest (Datatype_Data.get_all theory))
+              (Symtab.dest (Old_Datatype_Data.get_all theory))
      val corollaries' = map (Simplifier.simplify case_simpset) corollaries
      val extract = Rules.CONTEXT_REWRITE_RULE
                      (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)