src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

       | _ => rewrite_args args (pats, intro_t, ctxt))
     fun rewrite_prem atom =
       let
         val (_, args) = strip_comb atom
       in rewrite_args args end
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
     val intro_t = prop_of intro'
     val concl = Logic.strip_imp_concl intro_t
     val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
     val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)

 
 (* some peephole optimisations *)
 
 fun peephole_optimisation thy intro =
   let
-    val process = MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init thy))
+    val process =
+      MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy))
     fun process_False intro_t =
       if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
     fun process_True intro_t =
       map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t
   in