src/Pure/Isar/class_target.ML

   $> Element.eq_morphism thy (these_defs thy [class]);
 val export_morphism = #export_morph oo the_class_data;
 
 fun print_classes thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val algebra = Sign.classes_of thy;
     val arities =
       Symtab.empty
       |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
            Symtab.map_default (class, []) (insert (op =) tyco)) arities)

   let
     fun after_qed results =
       ProofContext.theory ((fold o fold) AxClass.add_classrel results);
   in
     thy
-    |> ProofContext.init
+    |> ProofContext.init_global
     |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
   end;
 
 in
 

   |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
   |> Option.map (fst o fst);
 
 fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
       (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
     val tycos = map #1 all_arities;
     val (_, sorts, sort) = hd all_arities;
     val vs = Name.names Name.context Name.aT sorts;

      of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
       | NONE => NONE;
   in
     thy
     |> Theory.checkpoint
-    |> ProofContext.init
+    |> ProofContext.init_global
     |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
     |> fold (Variable.declare_typ o TFree) vs
     |> fold (Variable.declare_names o Free o snd) params
     |> (Overloading.map_improvable_syntax o apfst)
          (K ((primary_constraints, []), (((improve, K NONE), false), [])))

   #> Local_Theory.exit_global;
 
 fun prove_instantiation_exit_result f tac x lthy =
   let
     val morph = ProofContext.export_morphism lthy
-      (ProofContext.init (ProofContext.theory_of lthy));
+      (ProofContext.init_global (ProofContext.theory_of lthy));
     val y = f morph x;
   in
     lthy
     |> prove_instantiation_exit (fn ctxt => tac ctxt y)
     |> pair y

     val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
     fun after_qed results = ProofContext.theory
       ((fold o fold) AxClass.add_arity results);
   in
     thy
-    |> ProofContext.init
+    |> ProofContext.init_global
     |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   end;
 
 
 (** tactics and methods **)