# HG changeset patch
# User wenzelm
# Date 1272889556 -7200
# Node ID bafd82950e2469a77bc880744fac9f3b7cad3b6a
# Parent  6ed6112f0a954a79db70f72c5d4bb4a03ca82fa2
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;

diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 03 14:25:56 2010 +0200
@@ -94,7 +94,7 @@
     fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
       | after_qed _ = I
   in
-    ProofContext.init thy
+    ProofContext.init_global thy
     |> fold Variable.auto_fixes ts
     |> (fn ctxt1 => ctxt1
     |> prepare
@@ -187,7 +187,7 @@
     end
 
   fun prove thy meth vc =
-    ProofContext.init thy
+    ProofContext.init_global thy
     |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
     |> Proof.apply meth
     |> Seq.hd
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Mon May 03 14:25:56 2010 +0200
@@ -232,7 +232,7 @@
     in apsnd sort_fst_str (fold split axs ([], [])) end
 
   fun mark_axioms thy axs =
-    Boogie_Axioms.get (ProofContext.init thy)
+    Boogie_Axioms.get (ProofContext.init_global thy)
     |> Termtab.make o map (fn thm => (Thm.prop_of thm, Unused thm))
     |> fold mark axs
     |> split_list_kind thy o Termtab.dest
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Mon May 03 14:25:56 2010 +0200
@@ -213,7 +213,7 @@
 fun smart_string_of_cterm ct =
     let
         val thy = Thm.theory_of_cterm ct
-        val ctxt = ProofContext.init thy
+        val ctxt = ProofContext.init_global thy
         val {t,T,...} = rep_cterm ct
         (* Hack to avoid parse errors with Trueprop *)
         val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Mutabelle/Mutabelle.thy
--- a/src/HOL/Mutabelle/Mutabelle.thy	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy	Mon May 03 14:25:56 2010 +0200
@@ -61,16 +61,16 @@
 
 (*
 ML {*
-Quickcheck.test_term (ProofContext.init @{theory})
+Quickcheck.test_term (ProofContext.init_global @{theory})
  false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps}))
 *}
 
 ML {*
 fun is_executable thy th = can (Quickcheck.test_term
- (ProofContext.init thy) false (SOME "SML") 1 1) (prop_of th);
+ (ProofContext.init_global thy) false (SOME "SML") 1 1) (prop_of th);
 
 fun is_executable_term thy t = can (Quickcheck.test_term
- (ProofContext.init thy) false (SOME "SML") 1 1) t;
+ (ProofContext.init_global thy) false (SOME "SML") 1 1) t;
 
 fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
    Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Mon May 03 14:25:56 2010 +0200
@@ -499,14 +499,14 @@
 
 fun is_executable thy insts th =
  (Quickcheck.test_term
-    (ProofContext.init thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
+    (ProofContext.init_global thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
   priority "executable"; true) handle ERROR s =>
     (priority ("not executable: " ^ s); false);
 
 fun qc_recursive usedthy [] insts sz qciter acc = rev acc
  | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
      (priority ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
-       (ProofContext.init usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
+       (ProofContext.init_global usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
           handle ERROR msg => (priority msg; qc_recursive usedthy xs insts sz qciter acc);
 
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon May 03 14:25:56 2010 +0200
@@ -97,7 +97,7 @@
 fun invoke_quickcheck quickcheck_generator thy t =
   TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
       (fn _ =>
-          case Quickcheck.gen_test_term (ProofContext.init thy) true true (SOME quickcheck_generator)
+          case Quickcheck.gen_test_term (ProofContext.init_global thy) true true (SOME quickcheck_generator)
                                     size iterations (preprocess thy [] t) of
             (NONE, (time_report, report)) => (NoCex, (time_report, report))
           | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
@@ -133,7 +133,7 @@
 
 fun invoke_nitpick thy t =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val state = Proof.init ctxt
   in
     let
@@ -251,7 +251,7 @@
   end
 
 fun is_executable_term thy t = can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) (Quickcheck.test_term
- (ProofContext.init thy) false (SOME "SML") 1 0)) (preprocess thy [] t)
+ (ProofContext.init_global thy) false (SOME "SML") 1 0)) (preprocess thy [] t)
 fun is_executable_thm thy th = is_executable_term thy (prop_of th)
 
 val freezeT =
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon May 03 14:25:56 2010 +0200
@@ -151,7 +151,7 @@
 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";
@@ -1617,7 +1617,7 @@
             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),
@@ -1712,7 +1712,7 @@
            (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
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 03 14:25:56 2010 +0200
@@ -124,7 +124,7 @@
   (* Find the variable we instantiate *)
   let
     val thy = theory_of_thm thm;
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val ss = global_simpset_of thy;
     val abs_fresh = PureThy.get_thms thy "abs_fresh";
     val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Mon May 03 14:25:56 2010 +0200
@@ -440,7 +440,7 @@
 
    fun string_of_typ T =
       setmp_CRITICAL show_sorts true
-       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
+       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
    val fixestate = (case state_type of
          NONE => []
        | SOME s =>
@@ -502,7 +502,7 @@
       *)
     val _ = writeln ("Defining statespace " ^ quote name ^ " ...");
 
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
 
     fun add_parent (Ts,pname,rs) env =
       let
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon May 03 14:25:56 2010 +0200
@@ -100,7 +100,7 @@
         val def' = Syntax.check_term lthy def;
         val ((_, (_, thm)), lthy') = Specification.definition
           (NONE, (Attrib.empty_binding, def')) lthy;
-        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+        val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;
     fun tac thms = Class.intro_classes_tac []
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 03 14:25:56 2010 +0200
@@ -165,7 +165,7 @@
 
 fun read_typ thy str sorts =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
       |> fold (Variable.declare_typ o TFree) sorts;
     val T = Syntax.read_typ ctxt str;
   in (T, Term.add_tfreesT T sorts) end;
@@ -316,7 +316,7 @@
     val (splits, thy9) = Datatype_Abs_Proofs.prove_split_thms
       config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
 
-    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
+    val inducts = Project_Rule.projections (ProofContext.init_global thy2) induct;
     val dt_infos = map_index
       (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
       (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
@@ -435,7 +435,7 @@
       end;
   in
     thy
-    |> ProofContext.init
+    |> ProofContext.init_global
     |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
   end;
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Function/size.ML	Mon May 03 14:25:56 2010 +0200
@@ -133,7 +133,7 @@
         val (thm, lthy') = lthy
           |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
           |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
-        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
+        val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy');
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;
 
@@ -152,7 +152,7 @@
       ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
       ||> Local_Theory.exit_global;
 
-    val ctxt = ProofContext.init thy';
+    val ctxt = ProofContext.init_global thy';
 
     val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
       size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 03 14:25:56 2010 +0200
@@ -286,7 +286,7 @@
   end
 
 fun default_params thy =
-  extract_params (ProofContext.init thy) false (default_raw_params thy)
+  extract_params (ProofContext.init_global thy) false (default_raw_params thy)
   o map (apsnd single)
 
 val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon May 03 14:25:56 2010 +0200
@@ -778,7 +778,7 @@
       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
@@ -860,7 +860,8 @@
 
 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 =
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon May 03 14:25:56 2010 +0200
@@ -580,7 +580,7 @@
     fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
        HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
      | replace_eqs t = t
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
     val prems = Thm.prems_of elimrule
     val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
@@ -608,7 +608,7 @@
 val no_compilation = ([], ([], []))
 
 fun fetch_pred_data thy name =
-  case try (Inductive.the_inductive (ProofContext.init thy)) name of
+  case try (Inductive.the_inductive (ProofContext.init_global thy)) name of
     SOME (info as (_, result)) => 
       let
         fun is_intro_of intro =
@@ -621,7 +621,7 @@
         val pre_elim = nth (#elims result) index
         val pred = nth (#preds result) index
         val nparams = length (Inductive.params_of (#raw_induct result))
-        val ctxt = ProofContext.init thy
+        val ctxt = ProofContext.init_global thy
         val elim_t = mk_casesrule ctxt pred intros
         val elim =
           prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
@@ -636,7 +636,7 @@
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
 fun is_inductive_predicate thy name =
-  is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
+  is_some (try (Inductive.the_inductive (ProofContext.init_global thy)) name)
 
 fun depending_preds_of thy (key, value) =
   let
@@ -688,7 +688,7 @@
     val pred = Const (constname, T)
     val pre_elim = 
       (Drule.export_without_context o Skip_Proof.make_thm thy)
-      (mk_casesrule (ProofContext.init thy) pred pre_intros)
+      (mk_casesrule (ProofContext.init_global thy) pred pre_intros)
   in register_predicate (constname, pre_intros, pre_elim) thy end
 
 fun defined_function_of compilation pred =
@@ -1160,7 +1160,7 @@
 fun is_possible_output thy vs t =
   forall
     (fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
-      (non_invertible_subterms (ProofContext.init thy) t)
+      (non_invertible_subterms (ProofContext.init_global thy) t)
   andalso
     (forall (is_eqT o snd)
       (inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
@@ -1367,7 +1367,7 @@
           val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
         in (modes, modes) end
     val (in_ts, out_ts) = split_mode mode ts
-    val in_vs = maps (vars_of_destructable_term (ProofContext.init thy)) in_ts
+    val in_vs = maps (vars_of_destructable_term (ProofContext.init_global thy)) in_ts
     val out_vs = terms_vs out_ts
     fun known_vs_after p vs = (case p of
         Prem t => union (op =) vs (term_vs t)
@@ -1939,7 +1939,7 @@
 
 fun compile_pred options compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val compilation_modifiers = if pol then compilation_modifiers else
       negative_comp_modifiers_of compilation_modifiers
     val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
@@ -2072,11 +2072,11 @@
     val simprules = [defthm, @{thm eval_pred},
       @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
     val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
-    val introthm = Goal.prove (ProofContext.init thy)
+    val introthm = Goal.prove (ProofContext.init_global thy)
       (argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
     val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
     val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
-    val elimthm = Goal.prove (ProofContext.init thy)
+    val elimthm = Goal.prove (ProofContext.init_global thy)
       (argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
     val opt_neg_introthm =
       if is_all_input mode then
@@ -2090,7 +2090,7 @@
             Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps
               (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
             THEN rtac @{thm Predicate.singleI} 1
-        in SOME (Goal.prove (ProofContext.init thy) (argnames @ hoarg_names') []
+        in SOME (Goal.prove (ProofContext.init_global thy) (argnames @ hoarg_names') []
             neg_introtrm (fn _ => tac))
         end
       else NONE
@@ -2604,7 +2604,7 @@
 
 fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
   in
     Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
@@ -2667,7 +2667,7 @@
     val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
     val (preds, intrs) = unify_consts thy preds intrs
     val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs]
-      (ProofContext.init thy)
+      (ProofContext.init_global thy)
     val preds = map dest_Const preds
     val all_vs = terms_vs intrs
     val all_modes = 
@@ -2744,7 +2744,7 @@
         val nparams = nparams_of thy predname
         val elim' =
           (Drule.export_without_context o Skip_Proof.make_thm thy)
-          (mk_casesrule (ProofContext.init thy) nparams intros)
+          (mk_casesrule (ProofContext.init_global thy) nparams intros)
       in
         if not (Thm.equiv_thm (elim, elim')) then
           error "Introduction and elimination rules do not match!"
@@ -2757,7 +2757,7 @@
 
 fun add_code_equations thy preds result_thmss =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     fun add_code_equation (predname, T) (pred, result_thms) =
       let
         val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
@@ -3047,7 +3047,7 @@
     fun after_qed thms goal_ctxt =
       let
         val global_thms = ProofContext.export goal_ctxt
-          (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
+          (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms)
       in
         goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #>
           ((case compilation options of
@@ -3164,7 +3164,7 @@
           | DSeq => dseq_comp_modifiers
           | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
           | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
-        val t_pred = compile_expr comp_modifiers (ProofContext.init thy)
+        val t_pred = compile_expr comp_modifiers (ProofContext.init_global thy)
           (body, deriv) additional_arguments;
         val T_pred = dest_predT compfuns (fastype_of t_pred)
         val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon May 03 14:25:56 2010 +0200
@@ -129,7 +129,7 @@
   
 fun split_all_pairs thy th =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val ((_, [th']), ctxt') = Variable.import true [th] ctxt
     val t = prop_of th'
     val frees = Term.add_frees t [] 
@@ -153,7 +153,7 @@
 
 fun inline_equations thy th =
   let
-    val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init thy)
+    val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init_global thy)
     val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th
     (*val _ = print_step options 
       ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
@@ -188,7 +188,7 @@
         tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
           " with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
       else ()
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     fun filtering th =
       if is_equationlike th andalso
         defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon May 03 14:25:56 2010 +0200
@@ -195,7 +195,7 @@
           SOME raw_split_thm =>
           let
             val (f, args) = strip_comb t
-            val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
+            val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
             val (assms, concl) = Logic.strip_horn (prop_of split_thm)
             val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
             val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon May 03 14:25:56 2010 +0200
@@ -64,7 +64,7 @@
 fun instantiated_case_rewrites thy Tcon =
   let
     val rew_ths = case_rewrites thy Tcon
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     fun instantiate th =
     let
       val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
@@ -128,9 +128,10 @@
       | SOME raw_split_thm =>
         let
           val (f, args) = strip_comb atom
-          val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
+          val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
           (* TODO: contextify things - this line is to unvarify the split_thm *)
-          (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
+          (*val ((_, [isplit_thm]), _) =
+            Variable.import true [split_thm] (ProofContext.init_global thy)*)
           val (assms, concl) = Logic.strip_horn (prop_of split_thm)
           val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
           val Tcons = datatype_names_of_case_name thy (fst (dest_Const f))
@@ -188,7 +189,7 @@
 
 fun flatten_intros constname intros thy =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val ((_, intros), ctxt') = Variable.import true intros ctxt
     val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
       (flatten constname) (map prop_of intros) ([], thy)
@@ -206,7 +207,7 @@
 
 fun introrulify thy ths = 
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val ((_, ths'), ctxt') = Variable.import true ths ctxt
     fun introrulify' th =
       let
@@ -277,7 +278,7 @@
     SOME specss => (specss, thy)
   | NONE =>*)
     let
-      val ctxt = ProofContext.init thy
+      val ctxt = ProofContext.init_global thy
       val intros =
         if forall is_pred_equation specs then 
           map (map_term thy (maps_premises (split_conjs thy))) (introrulify thy (map rewrite specs))
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon May 03 14:25:56 2010 +0200
@@ -200,7 +200,7 @@
       (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
        HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
     val tac = fn _ => Skip_Proof.cheat_tac thy1
-    val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac
+    val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
     val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
     val (thy3, preproc_time) = cpu_time "predicate preprocessing"
         (fn () => Predicate_Compile.preprocess options const thy2)
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon May 03 14:25:56 2010 +0200
@@ -65,7 +65,7 @@
 
 fun specialise_intros black_list (pred, intros) pats thy =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
     val pats = map (Logic.incr_indexes ([],  maxidx + 1)) pats
     val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Mon May 03 14:25:56 2010 +0200
@@ -140,7 +140,7 @@
 
 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
    let
-       val ctxt = ProofContext.init thy
+       val ctxt = ProofContext.init_global thy
        val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
        val {rules,rows,TCs,full_pats_TCs} =
            Prim.post_definition congs (thy, (def,pats))
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/TFL/rules.ML
--- a/src/HOL/Tools/TFL/rules.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML	Mon May 03 14:25:56 2010 +0200
@@ -814,7 +814,7 @@
   let
     val thy = Thm.theory_of_cterm ptm;
     val t = Thm.term_of ptm;
-    val ctxt = ProofContext.init thy |> Variable.auto_fixes t;
+    val ctxt = ProofContext.init_global thy |> Variable.auto_fixes t;
   in
     if strict then Goal.prove ctxt [] [] t (K tac)
     else Goal.prove ctxt [] [] t (K tac)
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon May 03 14:25:56 2010 +0200
@@ -361,7 +361,7 @@
 
 (*For Isabelle, the lhs of a definition must be a constant.*)
 fun const_def sign (c, Ty, rhs) =
-  singleton (Syntax.check_terms (ProofContext.init sign))
+  singleton (Syntax.check_terms (ProofContext.init_global sign))
     (Const("==",dummyT) $ Const(c,Ty) $ rhs);
 
 (*Make all TVars available for instantiation by adding a ? to the front*)
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Mon May 03 14:25:56 2010 +0200
@@ -225,7 +225,7 @@
         #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
     in
       thy
-      |> ProofContext.init
+      |> ProofContext.init_global
       |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon May 03 14:25:56 2010 +0200
@@ -66,7 +66,7 @@
           val nparms = (case optnparms of
             SOME k => k
           | NONE => (case rules of
-             [] => (case try (Inductive.the_inductive (ProofContext.init thy)) s of
+             [] => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
                  SOME (_, {raw_induct, ...}) =>
                    length (Inductive.params_of raw_induct)
                | NONE => 0)
@@ -84,7 +84,7 @@
 fun get_clauses thy s =
   let val {intros, graph, ...} = CodegenData.get thy
   in case Symtab.lookup intros s of
-      NONE => (case try (Inductive.the_inductive (ProofContext.init thy)) s of
+      NONE => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
         NONE => NONE
       | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
           SOME (names, Codegen.thyname_of_const thy s,
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon May 03 14:25:56 2010 +0200
@@ -137,7 +137,7 @@
 
 fun fun_of_prem thy rsets vs params rule ivs intr =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
     val args = map (Free o apfst fst o dest_Var) ivs;
     val args' = map (Free o apfst fst)
       (subtract (op =) params (Term.add_vars (prop_of intr) []));
@@ -484,7 +484,7 @@
 fun add_ind_realizers name rsets thy =
   let
     val (_, {intrs, induct, raw_induct, elims, ...}) =
-      Inductive.the_inductive (ProofContext.init thy) name;
+      Inductive.the_inductive (ProofContext.init_global thy) name;
     val vss = sort (int_ord o pairself length)
       (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
   in
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Mon May 03 14:25:56 2010 +0200
@@ -214,7 +214,7 @@
                                 fs @ map Bound (0 ::(length ls downto 1))))
     val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def";
     val def_prop =
-      singleton (Syntax.check_terms (ProofContext.init thy))
+      singleton (Syntax.check_terms (ProofContext.init_global thy))
         (Logic.mk_equals (Const (fname, dummyT), rhs));
   in (def_name, def_prop) end;
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/recdef.ML	Mon May 03 14:25:56 2010 +0200
@@ -160,7 +160,7 @@
 
 fun prepare_hints thy opt_src =
   let
-    val ctxt0 = ProofContext.init thy;
+    val ctxt0 = ProofContext.init_global thy;
     val ctxt =
       (case opt_src of
         NONE => ctxt0
@@ -172,7 +172,7 @@
 
 fun prepare_hints_i thy () =
   let
-    val ctxt0 = ProofContext.init thy;
+    val ctxt0 = ProofContext.init_global thy;
     val {simps, congs, wfs} = get_global_hints thy;
   in (claset_of ctxt0, simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
 
@@ -234,7 +234,7 @@
     val _ = requires_recdef thy;
     val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
 
-    val congs = eval_thms (ProofContext.init thy) raw_congs;
+    val congs = eval_thms (ProofContext.init_global thy) raw_congs;
     val (thy2, induct_rules) = tfl_fn thy congs name eqs;
     val ([induct_rules'], thy3) =
       thy2
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/record.ML	Mon May 03 14:25:56 2010 +0200
@@ -1038,7 +1038,7 @@
   let val thm =
     if ! quick_and_dirty then Skip_Proof.make_thm thy prop
     else if Goal.future_enabled () then
-      Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
+      Goal.future_result (ProofContext.init_global thy) (Future.fork_pri ~1 prf) prop
     else prf ()
   in Drule.export_without_context thm end;
 
@@ -1048,7 +1048,7 @@
       if ! quick_and_dirty then Skip_Proof.prove
       else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
       else Goal.prove_future;
-    val prf = prv (ProofContext.init thy) [] asms prop tac;
+    val prf = prv (ProofContext.init_global thy) [] asms prop tac;
   in if stndrd then Drule.export_without_context prf else prf end;
 
 val prove_future_global = prove_common false;
@@ -1090,7 +1090,7 @@
           else mk_comp_id acc;
         val prop = lhs === rhs;
         val othm =
-          Goal.prove (ProofContext.init thy) [] [] prop
+          Goal.prove (ProofContext.init_global thy) [] [] prop
             (fn _ =>
               simp_tac defset 1 THEN
               REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
@@ -1114,7 +1114,7 @@
       else mk_comp (u' $ f') (u $ f);
     val prop = lhs === rhs;
     val othm =
-      Goal.prove (ProofContext.init thy) [] [] prop
+      Goal.prove (ProofContext.init_global thy) [] [] prop
         (fn _ =>
           simp_tac defset 1 THEN
           REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
@@ -1155,7 +1155,7 @@
     val (_, args) = strip_comb lhs;
     val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
   in
-    Goal.prove (ProofContext.init thy) [] [] prop'
+    Goal.prove (ProofContext.init_global thy) [] [] prop'
       (fn _ =>
         simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
         TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
@@ -1247,7 +1247,7 @@
     val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)];
     val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
   in
-    Goal.prove (ProofContext.init thy) [] [] prop
+    Goal.prove (ProofContext.init_global thy) [] [] prop
       (fn _ =>
         simp_tac simpset 1 THEN
         REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
@@ -2388,7 +2388,7 @@
       if quiet_mode then ()
       else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
 
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T)
       handle TYPE (msg, _, _) => error msg;
 
@@ -2438,7 +2438,7 @@
 
 fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
     val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
     val (parent, ctxt2) = read_parent raw_parent ctxt1;
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML	Mon May 03 14:25:56 2010 +0200
@@ -52,7 +52,7 @@
 fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
   let
     val ty = Sign.certify_typ thy raw_ty;
-    val ctxt = ProofContext.init thy |> Variable.declare_typ ty;
+    val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
     val vs = map (ProofContext.check_tfree ctxt) raw_vs;
     val tac = Tactic.rtac UNIV_witness 1;
     fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Mon May 03 14:25:56 2010 +0200
@@ -182,7 +182,8 @@
         val thy = ProofContext.theory_of set_lthy;
         val cert = Thm.cterm_of thy;
         val (defs, A) =
-          Local_Defs.export_cterm set_lthy (ProofContext.init thy) (cert set') ||> Thm.term_of;
+          Local_Defs.export_cterm set_lthy (ProofContext.init_global thy) (cert set')
+          ||> Thm.term_of;
 
         val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
           Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 03 14:25:56 2010 +0200
@@ -189,7 +189,7 @@
         (K (beta_tac 1));
     val tuple_unfold_thm =
       (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
-      |> Local_Defs.unfold (ProofContext.init thy) @{thms split_conv};
+      |> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv};
 
     fun mk_unfold_thms [] thm = []
       | mk_unfold_thms (n::[]) thm = [(n, thm)]
@@ -380,7 +380,7 @@
 
 fun read_typ thy str sorts =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
       |> fold (Variable.declare_typ o TFree) sorts;
     val T = Syntax.read_typ ctxt str;
   in (T, Term.add_tfreesT T sorts) end;
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon May 03 14:25:56 2010 +0200
@@ -71,7 +71,7 @@
 end;
 
 fun legacy_infer_term thy t =
-  let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
+  let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init_global thy)
   in singleton (Syntax.check_terms ctxt) (intern_term thy t) end;
 
 fun pg'' thy defs t tacs =
@@ -347,7 +347,7 @@
 
 (* ----- theorems concerning finiteness and induction ----------------------- *)
 
-  val global_ctxt = ProofContext.init thy;
+  val global_ctxt = ProofContext.init_global thy;
 
   val _ = trace " Proving ind...";
   val ind =
@@ -422,7 +422,7 @@
           bot :: map (fn (c,_) => Long_Name.base_name c) cons;
   in adms @ flat (map2 one_eq bottoms eqs) end;
 
-val inducts = Project_Rule.projections (ProofContext.init thy) ind;
+val inducts = Project_Rule.projections (ProofContext.init_global thy) ind;
 fun ind_rule (dname, rule) =
     ((Binding.empty, [rule]),
      [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
@@ -470,7 +470,7 @@
 local
 
   fun legacy_infer_term thy t =
-      singleton (Syntax.check_terms (ProofContext.init thy)) (intern_term thy t);
+      singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
   fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
   fun infer_props thy = map (apsnd (legacy_infer_prop thy));
   fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML	Mon May 03 14:25:56 2010 +0200
@@ -170,7 +170,7 @@
 
     (*rhs*)
     val tmp_ctxt =
-      ProofContext.init thy
+      ProofContext.init_global thy
       |> fold (Variable.declare_typ o TFree) raw_args;
     val set = prep_term tmp_ctxt raw_set;
     val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
@@ -207,7 +207,7 @@
     val ((_, (_, below_ldef)), lthy4) = lthy3
       |> Specification.definition (NONE,
           ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
-    val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
+    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4);
     val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
     val thy5 = lthy4
       |> Class.prove_instantiation_instance
@@ -322,7 +322,7 @@
 fun gen_cpodef_proof prep_term prep_constraint
     ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val args = map (apsnd (prep_constraint ctxt)) raw_args;
     val (goal1, goal2, make_result) =
       prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
@@ -333,7 +333,7 @@
 fun gen_pcpodef_proof prep_term prep_constraint
     ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val args = map (apsnd (prep_constraint ctxt)) raw_args;
     val (goal1, goal2, make_result) =
       prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
diff -r 6ed6112f0a95 -r bafd82950e24 src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML	Mon May 03 14:25:56 2010 +0200
@@ -65,7 +65,7 @@
 
     (*rhs*)
     val tmp_ctxt =
-      ProofContext.init thy
+      ProofContext.init_global thy
       |> fold (Variable.declare_typ o TFree) raw_args;
     val defl = prep_term tmp_ctxt raw_defl;
     val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
@@ -119,7 +119,7 @@
         Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
     val ((_, (_, approx_ldef)), lthy) =
         Specification.definition (NONE, (approx_bind, approx_eqn)) lthy;
-    val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
     val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
     val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
     val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef;
@@ -161,7 +161,7 @@
 
 fun repdef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args;
   in snd (gen_add_repdef Syntax.read_term def name (b, args, mx) A morphs thy) end;
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Provers/classical.ML	Mon May 03 14:25:56 2010 +0200
@@ -210,7 +210,7 @@
 fun dup_elim th =
   let
     val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
-    val ctxt = ProofContext.init (Thm.theory_of_thm rl);
+    val ctxt = ProofContext.init_global (Thm.theory_of_thm rl);
   in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
 
 
@@ -856,7 +856,7 @@
 
 fun global_claset_of thy =
   let val (cs, ctxt_cs) = GlobalClaset.get thy
-  in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
+  in context_cs (ProofContext.init_global thy) cs (ctxt_cs) end;
 
 
 (* context dependent components *)
diff -r 6ed6112f0a95 -r bafd82950e24 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Provers/quantifier1.ML	Mon May 03 14:25:56 2010 +0200
@@ -113,7 +113,7 @@
   in exqu [] end;
 
 fun prove_conv tac thy tu =
-  Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
+  Goal.prove (ProofContext.init_global thy) [] [] (Logic.mk_equals tu)
     (K (rtac iff_reflection 1 THEN tac));
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/class.ML	Mon May 03 14:25:56 2010 +0200
@@ -32,7 +32,7 @@
 
 fun calculate thy class sups base_sort param_map assm_axiom =
   let
-    val empty_ctxt = ProofContext.init thy;
+    val empty_ctxt = ProofContext.init_global thy;
 
     (* instantiation of canonical interpretation *)
     val aT = TFree (Name.aT, base_sort);
@@ -143,7 +143,7 @@
       #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
     val raw_supexpr = (map (fn sup => (sup, (("", false),
       Expression.Positional []))) sups, []);
-    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
+    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy
       |> prep_decl raw_supexpr init_class_body raw_elems;
     fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
       | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
@@ -194,7 +194,7 @@
     val sup_sort = inter_sort base_sort sups;
 
     (* process elements as class specification *)
-    val class_ctxt = begin sups base_sort (ProofContext.init thy);
+    val class_ctxt = begin sups base_sort (ProofContext.init_global thy);
     val ((_, _, syntax_elems), _) = class_ctxt
       |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs = if null vs
@@ -340,7 +340,7 @@
 
 val subclass = gen_subclass (K I) user_proof;
 fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
-val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init) user_proof;
+val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
 
 end; (*local*)
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Mon May 03 14:25:56 2010 +0200
@@ -157,7 +157,7 @@
 
 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
@@ -372,7 +372,7 @@
       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;
 
@@ -421,7 +421,7 @@
 
 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;
@@ -514,7 +514,7 @@
   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
@@ -554,7 +554,7 @@
 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
@@ -597,7 +597,7 @@
       ((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;
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/code.ML	Mon May 03 14:25:56 2010 +0200
@@ -337,7 +337,7 @@
 fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
 
 fun read_signature thy = cert_signature thy o Type.strip_sorts
-  o Syntax.parse_typ (ProofContext.init thy);
+  o Syntax.parse_typ (ProofContext.init_global thy);
 
 fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
 
@@ -554,7 +554,7 @@
 
 fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
 
-fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init thy);
+fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy);
 
 fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
   apfst (meta_rewrite thy);
@@ -941,7 +941,7 @@
 
 fun print_codesetup thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val exec = the_exec thy;
     fun pretty_equations const thms =
       (Pretty.block o Pretty.fbreaks) (
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/constdefs.ML	Mon May 03 14:25:56 2010 +0200
@@ -26,7 +26,7 @@
 
     fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
 
-    val thy_ctxt = ProofContext.init thy;
+    val thy_ctxt = ProofContext.init_global thy;
     val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
     val ((d, mx), var_ctxt) =
       (case raw_decl of
@@ -62,7 +62,7 @@
 
 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
     val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
   in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Mon May 03 14:25:56 2010 +0200
@@ -642,7 +642,7 @@
       |> 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;
 
@@ -729,7 +729,7 @@
       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 =
@@ -795,7 +795,7 @@
 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;
@@ -809,7 +809,8 @@
         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
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon May 03 14:25:56 2010 +0200
@@ -181,7 +181,8 @@
   Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
 
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
-fun global_morphism lthy = standard_morphism lthy (ProofContext.init (ProofContext.theory_of lthy));
+fun global_morphism lthy =
+  standard_morphism lthy (ProofContext.init_global (ProofContext.theory_of lthy));
 
 
 (* primitive operations *)
@@ -270,7 +271,7 @@
 fun exit_result_global f (x, lthy) =
   let
     val thy = exit_global lthy;
-    val thy_ctxt = ProofContext.init thy;
+    val thy_ctxt = ProofContext.init_global thy;
     val phi = standard_morphism lthy thy_ctxt;
   in (f phi x, thy) end;
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Mon May 03 14:25:56 2010 +0200
@@ -308,7 +308,7 @@
 
 fun init name thy =
   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
-    ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
+    ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
 
 fun print_locale thy show_facts raw_name =
   let
@@ -412,7 +412,7 @@
   let
     val name = intern thy raw_name;
     val name' = extern thy name;
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
     fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/object_logic.ML	Mon May 03 14:25:56 2010 +0200
@@ -186,7 +186,7 @@
 fun atomize_prems ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
     Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
-      (ProofContext.init (Thm.theory_of_cterm ct)) ct
+      (ProofContext.init_global (Thm.theory_of_cterm ct)) ct
   else Conv.all_conv ct;
 
 val atomize_prems_tac = CONVERSION atomize_prems;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon May 03 14:25:56 2010 +0200
@@ -156,7 +156,7 @@
   in
     thy
     |> Theory.checkpoint
-    |> ProofContext.init
+    |> ProofContext.init_global
     |> OverloadingData.put overloading
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
     |> add_improvable_syntax
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon May 03 14:25:56 2010 +0200
@@ -9,7 +9,7 @@
 signature PROOF_CONTEXT =
 sig
   val theory_of: Proof.context -> theory
-  val init: theory -> Proof.context
+  val init_global: theory -> Proof.context
   type mode
   val mode_default: mode
   val mode_stmt: mode
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon May 03 14:25:56 2010 +0200
@@ -48,7 +48,7 @@
 
 fun pretty_theorems_diff verbose prev_thys thy =
   let
-    val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
+    val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy);
     val facts = PureThy.facts_of thy;
     val thmss =
       Facts.dest_static (map PureThy.facts_of prev_thys) facts
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Mon May 03 14:25:56 2010 +0200
@@ -39,6 +39,6 @@
       else tac args st);
 
 fun prove_global thy xs asms prop tac =
-  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
+  Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
 
 end;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Mon May 03 14:25:56 2010 +0200
@@ -169,7 +169,7 @@
 
 fun gen_axioms do_print prep raw_vars raw_specs thy =
   let
-    val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
+    val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init_global thy);
     val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
 
     (*consts*)
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon May 03 14:25:56 2010 +0200
@@ -114,7 +114,7 @@
 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;
 
@@ -213,7 +213,7 @@
 
 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;
@@ -286,7 +286,7 @@
 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;
 
@@ -342,7 +342,7 @@
 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;
 
@@ -364,7 +364,7 @@
 
 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;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Mon May 03 14:25:56 2010 +0200
@@ -206,7 +206,7 @@
       |> add_proof_syntax
       |> add_proof_atom_consts
         (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
-      |> ProofContext.init
+      |> ProofContext.init_global
       |> ProofContext.allow_dummies
       |> ProofContext.set_mode ProofContext.mode_schematic;
   in
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon May 03 14:25:56 2010 +0200
@@ -850,10 +850,10 @@
 val read_term = singleton o read_terms;
 val read_prop = singleton o read_props;
 
-val read_sort_global = read_sort o ProofContext.init;
-val read_typ_global = read_typ o ProofContext.init;
-val read_term_global = read_term o ProofContext.init;
-val read_prop_global = read_prop o ProofContext.init;
+val read_sort_global = read_sort o ProofContext.init_global;
+val read_typ_global = read_typ o ProofContext.init_global;
+val read_term_global = read_term o ProofContext.init_global;
+val read_prop_global = read_prop o ProofContext.init_global;
 
 
 (* pretty = uncheck + unparse *)
@@ -876,7 +876,7 @@
 structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
 val is_pretty_global = PrettyGlobal.get;
 val set_pretty_global = PrettyGlobal.put;
-val init_pretty_global = set_pretty_global true o ProofContext.init;
+val init_pretty_global = set_pretty_global true o ProofContext.init_global;
 
 val pretty_term_global = pretty_term o init_pretty_global;
 val pretty_typ_global = pretty_typ o init_pretty_global;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/axclass.ML	Mon May 03 14:25:56 2010 +0200
@@ -198,7 +198,7 @@
   (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
     SOME thm => Thm.transfer thy thm
   | NONE => error ("Unproven class relation " ^
-      Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
+      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));
 
 fun put_trancl_classrel ((c1, c2), th) thy =
   let
@@ -245,7 +245,7 @@
   (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
     SOME (thm, _) => Thm.transfer thy thm
   | NONE => error ("Unproven type arity " ^
-      Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
+      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));
 
 fun thynames_of_arity thy (c, a) =
   Symtab.lookup_list (proven_arities_of thy) a
@@ -357,7 +357,7 @@
   in (c1, c2) end;
 
 fun read_classrel thy raw_rel =
-  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
+  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init_global thy)) raw_rel)
     handle TYPE (msg, _, _) => error msg;
 
 
@@ -461,7 +461,7 @@
 
 fun prove_classrel raw_rel tac thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val (c1, c2) = cert_classrel thy raw_rel;
     val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
       cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
@@ -475,7 +475,7 @@
 
 fun prove_arity raw_arity tac thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val arity = ProofContext.cert_arity ctxt raw_arity;
     val names = map (prefix arity_prefix) (Logic.name_arities arity);
     val props = Logic.mk_arities arity;
@@ -509,7 +509,7 @@
 
 fun define_class (bclass, raw_super) raw_params raw_specs thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val pp = Syntax.pp ctxt;
 
 
@@ -623,7 +623,7 @@
     (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
 
 fun ax_arity prep =
-  axiomatize (prep o ProofContext.init) Logic.mk_arities
+  axiomatize (prep o ProofContext.init_global) Logic.mk_arities
     (map (prefix arity_prefix) o Logic.name_arities) add_arity;
 
 fun class_const c =
@@ -643,7 +643,7 @@
 in
 
 val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel;
+val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init_global) read_classrel;
 val axiomatize_classrel = ax_classrel cert_classrel;
 val axiomatize_classrel_cmd = ax_classrel read_classrel;
 val axiomatize_arity = ax_arity ProofContext.cert_arity;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/codegen.ML	Mon May 03 14:25:56 2010 +0200
@@ -822,7 +822,7 @@
 
 val generate_code_i = gen_generate_code Sign.cert_term;
 val generate_code =
-  gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init);
+  gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init_global);
 
 
 (**** Reflection ****)
@@ -908,7 +908,7 @@
 
 fun eval_term thy t =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val e =
       let
         val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/context.ML	Mon May 03 14:25:56 2010 +0200
@@ -20,7 +20,7 @@
   structure ProofContext:
   sig
     val theory_of: Proof.context -> theory
-    val init: theory -> Proof.context
+    val init_global: theory -> Proof.context
   end
 end;
 
@@ -481,7 +481,7 @@
 structure ProofContext =
 struct
   val theory_of = theory_of_proof;
-  fun init thy = Proof.Context (init_data thy, check_thy thy);
+  fun init_global thy = Proof.Context (init_data thy, check_thy thy);
 end;
 
 structure Proof_Data =
@@ -529,7 +529,7 @@
 fun proof_map f = the_proof o f o Proof;
 
 val theory_of = cases I ProofContext.theory_of;
-val proof_of = cases ProofContext.init I;
+val proof_of = cases ProofContext.init_global I;
 
 
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/goal.ML	Mon May 03 14:25:56 2010 +0200
@@ -211,7 +211,7 @@
 fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
 
 fun prove_global thy xs asms prop tac =
-  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
+  Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
 
 
 
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon May 03 14:25:56 2010 +0200
@@ -299,7 +299,7 @@
 in
 
 fun print_term_global ss warn a thy t =
-  print_term ss warn (K a) t (ProofContext.init thy);
+  print_term ss warn (K a) t (ProofContext.init_global thy);
 
 fun if_enabled (Simpset ({context, ...}, _)) flag f =
   (case context of
@@ -355,7 +355,7 @@
 fun context ctxt =
   map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
 
-val global_context = context o ProofContext.init;
+val global_context = context o ProofContext.init_global;
 
 fun activate_context thy ss =
   let
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/old_goals.ML	Mon May 03 14:25:56 2010 +0200
@@ -219,7 +219,7 @@
 
 fun simple_read_term thy T s =
   let
-    val ctxt = ProofContext.init thy
+    val ctxt = ProofContext.init_global thy
       |> ProofContext.allow_dummies
       |> ProofContext.set_mode ProofContext.mode_schematic;
     val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/sign.ML	Mon May 03 14:25:56 2010 +0200
@@ -361,7 +361,7 @@
 
 fun gen_syntax change_gram parse_typ mode args thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
       handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
   in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
@@ -398,7 +398,7 @@
 
 fun gen_add_consts parse_typ raw_args thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
     fun prep (b, raw_T, mx) =
       let
@@ -497,7 +497,7 @@
 
 fun gen_trrules f args thy = thy |> map_syn (fn syn =>
   let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
-  in f (ProofContext.init thy) (is_logtype thy) syn rules syn end);
+  in f (ProofContext.init_global thy) (is_logtype thy) syn rules syn end);
 
 val add_trrules = gen_trrules Syntax.update_trrules;
 val del_trrules = gen_trrules Syntax.remove_trrules;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/simplifier.ML	Mon May 03 14:25:56 2010 +0200
@@ -127,7 +127,7 @@
 fun map_simpset f = Context.theory_map (map_ss f);
 fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
 fun global_simpset_of thy =
-  MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
+  MetaSimplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy));
 
 fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
 fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/theory.ML	Mon May 03 14:25:56 2010 +0200
@@ -238,7 +238,7 @@
 
 fun check_def thy unchecked overloaded (b, tm) defs =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val name = Sign.full_name thy b;
     val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
       handle TERM (msg, _) => error msg;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/variable.ML	Mon May 03 14:25:56 2010 +0200
@@ -235,7 +235,7 @@
 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
 
 val declare_thm = Thm.fold_terms declare_internal;
-fun global_thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
+fun global_thm_context th = declare_thm th (ProofContext.init_global (Thm.theory_of_thm th));
 
 
 (* renaming term/type frees *)
diff -r 6ed6112f0a95 -r bafd82950e24 src/Tools/Code/code_eval.ML
--- a/src/Tools/Code/code_eval.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Mon May 03 14:25:56 2010 +0200
@@ -47,7 +47,7 @@
 
 fun eval some_target reff postproc thy t args =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     fun evaluator naming program ((_, (_, ty)), t) deps =
       let
         val _ = if Code_Thingol.contains_dictvar t then
diff -r 6ed6112f0a95 -r bafd82950e24 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon May 03 14:25:56 2010 +0200
@@ -87,7 +87,7 @@
 
 fun add_unfold_post raw_thm thy =
   let
-    val thm = Local_Defs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
+    val thm = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) raw_thm;
     val thm_sym = Thm.symmetric thm;
   in
     thy |> map_pre_post (fn (pre, post) =>
@@ -157,7 +157,7 @@
 
 fun print_codeproc thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val pre = (#pre o the_thmproc) thy;
     val post = (#post o the_thmproc) thy;
     val functrans = (map fst o #functrans o the_thmproc) thy;
diff -r 6ed6112f0a95 -r bafd82950e24 src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 03 14:25:56 2010 +0200
@@ -210,7 +210,7 @@
 
     fun do_find () =
       let
-        val ctxt = ProofContext.init (theory thy_name);
+        val ctxt = ProofContext.init_global (theory thy_name);
         val query = get_query ();
         val (othmslen, thms) = apsnd rev
           (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
diff -r 6ed6112f0a95 -r bafd82950e24 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Tools/nbe.ML	Mon May 03 14:25:56 2010 +0200
@@ -521,7 +521,7 @@
 
 fun compile_eval thy program vs_t deps =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val (gr, (_, idx_tab)) =
       Nbe_Functions.change thy (ensure_stmts ctxt program);
   in
diff -r 6ed6112f0a95 -r bafd82950e24 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Tools/quickcheck.ML	Mon May 03 14:25:56 2010 +0200
@@ -295,7 +295,7 @@
 
 fun quickcheck_params_cmd args thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val f = fold (parse_test_param ctxt) args;
   in
     thy
diff -r 6ed6112f0a95 -r bafd82950e24 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Mon May 03 14:25:56 2010 +0200
@@ -401,7 +401,7 @@
 
 fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     fun read_is strs =
       map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
       |> Syntax.check_terms ctxt;
diff -r 6ed6112f0a95 -r bafd82950e24 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Mon May 03 14:25:56 2010 +0200
@@ -46,7 +46,7 @@
 
 fun inductive_cases args thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val facts = args |> map (fn ((name, srcs), props) =>
       ((name, map (Attrib.attribute thy) srcs),
         map (Thm.no_attributes o single o smart_cases ctxt) props));
diff -r 6ed6112f0a95 -r bafd82950e24 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Mon May 03 14:25:56 2010 +0200
@@ -163,7 +163,7 @@
 
 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
     val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
     val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
diff -r 6ed6112f0a95 -r bafd82950e24 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Mon May 03 14:25:56 2010 +0200
@@ -62,7 +62,7 @@
   raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
 let
   val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
-  val ctxt = ProofContext.init thy;
+  val ctxt = ProofContext.init_global thy;
 
   val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
   val (intr_names, intr_tms) = split_list (map fst intr_specs);
@@ -174,7 +174,7 @@
     |> Sign.add_path big_rec_base_name
     |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
 
-  val ctxt1 = ProofContext.init thy1;
+  val ctxt1 = ProofContext.init_global thy1;
 
 
   (*fetch fp definitions from the theory*)
@@ -261,7 +261,7 @@
       THEN (PRIMITIVE (fold_rule part_rec_defs));
 
   (*Elimination*)
-  val elim = rule_by_tactic (ProofContext.init thy1) basic_elim_tac
+  val elim = rule_by_tactic (ProofContext.init_global thy1) basic_elim_tac
                  (unfold RS Ind_Syntax.equals_CollectD)
 
   (*Applies freeness of the given constructors, which *must* be unfolded by
@@ -554,7 +554,7 @@
 fun add_inductive (srec_tms, sdom_sum) intr_srcs
     (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   let
-    val ctxt = ProofContext.init thy;
+    val ctxt = ProofContext.init_global thy;
     val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
       #> Syntax.check_terms ctxt;