src/HOL/Tools/TFL/tfl.ML

                            given_pats
      val (case_rewrites,context_congs) = extraction_thms theory
      (*case_ss causes minimal simplification: bodies of case expressions are
        not simplified. Otherwise large examples (Red-Black trees) are too
        slow.*)
-     val case_ss =
-       Simplifier.global_context theory
-         (HOL_basic_ss addsimps case_rewrites
+     val case_simpset =
+       Simplifier.global_context theory HOL_basic_ss
+          addsimps case_rewrites
           |> fold (Simplifier.add_cong o #weak_case_cong o snd)
-              (Symtab.dest (Datatype.get_all theory)))
-     val corollaries' = map (Simplifier.simplify case_ss) corollaries
+              (Symtab.dest (Datatype.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)
+                     (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
      val (rules, TCs) = ListPair.unzip (map extract corollaries')
      val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
      val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
      val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
  in