src/HOL/Tools/TFL/tfl.ML

        slow.*)
      val case_simpset =
        put_simpset HOL_basic_ss ctxt
           addsimps case_rewrites
           |> fold (Simplifier.add_cong o #case_cong_weak o snd)
-              (Symtab.dest (Datatype.get_all theory))
+              (Symtab.dest (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)
      val (rules, TCs) = ListPair.unzip (map extract corollaries')
      val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules