src/Pure/Isar/object_logic.ML

   MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
 
 fun atomize_prems ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
     Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
-      (ProofContext.init (Thm.theory_of_cterm ct)) ct
+      (ProofContext.init_global (Thm.theory_of_cterm ct)) ct
   else Conv.all_conv ct;
 
 val atomize_prems_tac = CONVERSION atomize_prems;
 val full_atomize_tac = CONVERSION atomize;