src/HOL/Tools/TFL/tfl.ML

      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_simpset =
-       put_simpset HOL_basic_ss (Proof_Context.init_global theory)
+       put_simpset HOL_basic_ss ctxt
           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_simpset) corollaries
      val extract = Rules.CONTEXT_REWRITE_RULE