src/Pure/Isar/expression.ML

       thy
       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
       |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
       |> PureThy.add_defs false
         [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
-    val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
+    val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
 
     val cert = Thm.cterm_of defs_thy;
 
     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
       MetaSimplifier.rewrite_goals_tac [pred_def] THEN

     val name = Sign.full_name thy binding;
     val _ = Locale.defined thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
     val ((fixed, deps, body_elems), (parms, ctxt')) =
-      prep_decl raw_import I raw_body (ProofContext.init thy);
+      prep_decl raw_import I raw_body (ProofContext.init_global thy);
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
     val predicate_binding =
       if Binding.is_empty raw_predicate_binding then binding
       else raw_predicate_binding;

 local
 
 fun gen_interpretation prep_expr parse_prop prep_attr
     expression equations theory =
   let
-    val ((propss, deps, export), expr_ctxt) = ProofContext.init theory
+    val ((propss, deps, export), expr_ctxt) = ProofContext.init_global theory
       |> prep_expr expression;
 
     val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
     val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
     val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;

       let
         val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
         val eqn_attrss = map2 (fn attrs => fn eqn =>
           ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
         fun meta_rewrite thy =
-          map (Local_Defs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def) o maps snd;
+          map (Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) #> Drule.abs_def) o
+            maps snd;
       in
         thy
         |> PureThy.note_thmss Thm.lemmaK eqn_attrss
         |-> (fn facts => `(fn thy => meta_rewrite thy facts))
       end;