src/Pure/Isar/theory_target.ML

 (* notes *)
 
 fun import_export_proof ctxt (name, raw_th) =
   let
     val thy = ProofContext.theory_of ctxt;
-    val thy_ctxt = ProofContext.init thy;
+    val thy_ctxt = ProofContext.init_global thy;
     val certT = Thm.ctyp_of thy;
     val cert = Thm.cterm_of thy;
 
     (*export assumes/defines*)
     val th = Goal.norm_result raw_th;

 
 (* abbrev *)
 
 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   let
-    val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
+    val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
     val target_ctxt = Local_Theory.target_of lthy;
 
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
     val t' = Assumption.export_term lthy target_ctxt t;
     val xs = map Free (rev (Variable.add_fixed target_ctxt t' []));

 in
 
 fun define ta ((b, mx), ((name, atts), rhs)) lthy =
   let
     val thy = ProofContext.theory_of lthy;
-    val thy_ctxt = ProofContext.init thy;
+    val thy_ctxt = ProofContext.init_global thy;
 
     val name' = Thm.def_binding_optional b name;
 
     val crhs = Thm.cterm_of thy rhs;
     val (defs, rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;

       else error ("No such locale: " ^ quote target);
 
 fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
   if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
   else if not (null overloading) then Overloading.init overloading
-  else if not is_locale then ProofContext.init
+  else if not is_locale then ProofContext.init_global
   else if not is_class then Locale.init target
   else Class_Target.init target;
 
 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
   Data.put ta #>

        else I)}
 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
 
 fun gen_overloading prep_const raw_ops thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val ops = raw_ops |> map (fn (name, const, checked) =>
       (name, Term.dest_Const (prep_const ctxt const), checked));
   in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
 
 in