src/FOL/simpdata.ML

 fun   safe_solver prems = FIRST'[match_tac (triv_rls @ prems),
                                  eq_assume_tac, ematch_tac [@{thm FalseE}]];
 
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss =
-  Simplifier.theory_context @{theory} empty_ss
+  Simplifier.global_context @{theory} empty_ss
   setsubgoaler asm_simp_tac
   setSSolver (mk_solver "FOL safe" safe_solver)
   setSolver (mk_solver "FOL unsafe" unsafe_solver)
   setmksimps (mksimps mksimps_pairs)
   setmkcong mk_meta_cong;