src/HOL/Nominal/nominal_datatype.ML

   Simplifier.simproc @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
 
 val meta_spec = thm "meta_spec";
 
 fun projections rule =
-  Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
+  Project_Rule.projections (ProofContext.init_global (Thm.theory_of_thm rule)) rule
   |> map (Drule.export_without_context #> Rule_Cases.save rule);
 
 val supp_prod = thm "supp_prod";
 val fresh_prod = thm "fresh_prod";
 val supports_fresh = thm "supports_fresh";

           let
             val x = Free ("x", augment_sort_typ thy11 fs_cp_sort T);
             val y = Free ("y", U);
             val y' = Free ("y'", U)
           in
-            Drule.export_without_context (Goal.prove (ProofContext.init thy11) []
+            Drule.export_without_context (Goal.prove (ProofContext.init_global thy11) []
               (map (augment_sort thy11 fs_cp_sort)
                 (finite_prems @
                    [HOLogic.mk_Trueprop (R $ x $ y),
                     HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U,
                       HOLogic.mk_imp (R $ x $ y', HOLogic.mk_eq (y', y)))),

       HOLogic.mk_Trueprop
         (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
            (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
 
     val rec_unique_thms = split_conj_thm (Goal.prove
-      (ProofContext.init thy11) (map fst rec_unique_frees)
+      (ProofContext.init_global thy11) (map fst rec_unique_frees)
       (map (augment_sort thy11 fs_cp_sort)
         (flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
       (augment_sort thy11 fs_cp_sort
         (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls)))
       (fn {prems, context} =>