renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
authorwenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610bafd82950e24
parent 36609 6ed6112f0a95
child 36611 b0c047d03208
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Mutabelle/Mutabelle.thy
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typecopy.ML
src/HOL/Tools/typedef.ML
src/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tools/repdef.ML
src/Provers/classical.ML
src/Provers/quantifier1.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/code.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/skip_proof.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Syntax/syntax.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/context.ML
src/Pure/goal.ML
src/Pure/meta_simplifier.ML
src/Pure/old_goals.ML
src/Pure/sign.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
src/Pure/variable.ML
src/Tools/Code/code_eval.ML
src/Tools/Code/code_preproc.ML
src/Tools/WWW_Find/find_theorems.ML
src/Tools/nbe.ML
src/Tools/quickcheck.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4      fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
     1.5        | after_qed _ = I
     1.6    in
     1.7 -    ProofContext.init thy
     1.8 +    ProofContext.init_global thy
     1.9      |> fold Variable.auto_fixes ts
    1.10      |> (fn ctxt1 => ctxt1
    1.11      |> prepare
    1.12 @@ -187,7 +187,7 @@
    1.13      end
    1.14  
    1.15    fun prove thy meth vc =
    1.16 -    ProofContext.init thy
    1.17 +    ProofContext.init_global thy
    1.18      |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
    1.19      |> Proof.apply meth
    1.20      |> Seq.hd
     2.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Mon May 03 07:59:51 2010 +0200
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Mon May 03 14:25:56 2010 +0200
     2.3 @@ -232,7 +232,7 @@
     2.4      in apsnd sort_fst_str (fold split axs ([], [])) end
     2.5  
     2.6    fun mark_axioms thy axs =
     2.7 -    Boogie_Axioms.get (ProofContext.init thy)
     2.8 +    Boogie_Axioms.get (ProofContext.init_global thy)
     2.9      |> Termtab.make o map (fn thm => (Thm.prop_of thm, Unused thm))
    2.10      |> fold mark axs
    2.11      |> split_list_kind thy o Termtab.dest
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Mon May 03 07:59:51 2010 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon May 03 14:25:56 2010 +0200
     3.3 @@ -213,7 +213,7 @@
     3.4  fun smart_string_of_cterm ct =
     3.5      let
     3.6          val thy = Thm.theory_of_cterm ct
     3.7 -        val ctxt = ProofContext.init thy
     3.8 +        val ctxt = ProofContext.init_global thy
     3.9          val {t,T,...} = rep_cterm ct
    3.10          (* Hack to avoid parse errors with Trueprop *)
    3.11          val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
     4.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Mon May 03 07:59:51 2010 +0200
     4.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Mon May 03 14:25:56 2010 +0200
     4.3 @@ -61,16 +61,16 @@
     4.4  
     4.5  (*
     4.6  ML {*
     4.7 -Quickcheck.test_term (ProofContext.init @{theory})
     4.8 +Quickcheck.test_term (ProofContext.init_global @{theory})
     4.9   false (SOME "SML") 1 1 (prop_of (hd @{thms nibble_pair_of_char_simps}))
    4.10  *}
    4.11  
    4.12  ML {*
    4.13  fun is_executable thy th = can (Quickcheck.test_term
    4.14 - (ProofContext.init thy) false (SOME "SML") 1 1) (prop_of th);
    4.15 + (ProofContext.init_global thy) false (SOME "SML") 1 1) (prop_of th);
    4.16  
    4.17  fun is_executable_term thy t = can (Quickcheck.test_term
    4.18 - (ProofContext.init thy) false (SOME "SML") 1 1) t;
    4.19 + (ProofContext.init_global thy) false (SOME "SML") 1 1) t;
    4.20  
    4.21  fun thms_of thy = filter (fn (_, th) => not (Thm.is_internal th) andalso
    4.22     Context.theory_name (theory_of_thm th) = Context.theory_name thy andalso
     5.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Mon May 03 07:59:51 2010 +0200
     5.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Mon May 03 14:25:56 2010 +0200
     5.3 @@ -499,14 +499,14 @@
     5.4  
     5.5  fun is_executable thy insts th =
     5.6   (Quickcheck.test_term
     5.7 -    (ProofContext.init thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
     5.8 +    (ProofContext.init_global thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th));
     5.9    priority "executable"; true) handle ERROR s =>
    5.10      (priority ("not executable: " ^ s); false);
    5.11  
    5.12  fun qc_recursive usedthy [] insts sz qciter acc = rev acc
    5.13   | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
    5.14       (priority ("qc_recursive: " ^ string_of_int (length xs)); ((x, pretty (the_default [] (Quickcheck.test_term
    5.15 -       (ProofContext.init usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
    5.16 +       (ProofContext.init_global usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc))
    5.17            handle ERROR msg => (priority msg; qc_recursive usedthy xs insts sz qciter acc);
    5.18  
    5.19  
     6.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon May 03 07:59:51 2010 +0200
     6.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon May 03 14:25:56 2010 +0200
     6.3 @@ -97,7 +97,7 @@
     6.4  fun invoke_quickcheck quickcheck_generator thy t =
     6.5    TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
     6.6        (fn _ =>
     6.7 -          case Quickcheck.gen_test_term (ProofContext.init thy) true true (SOME quickcheck_generator)
     6.8 +          case Quickcheck.gen_test_term (ProofContext.init_global thy) true true (SOME quickcheck_generator)
     6.9                                      size iterations (preprocess thy [] t) of
    6.10              (NONE, (time_report, report)) => (NoCex, (time_report, report))
    6.11            | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
    6.12 @@ -133,7 +133,7 @@
    6.13  
    6.14  fun invoke_nitpick thy t =
    6.15    let
    6.16 -    val ctxt = ProofContext.init thy
    6.17 +    val ctxt = ProofContext.init_global thy
    6.18      val state = Proof.init ctxt
    6.19    in
    6.20      let
    6.21 @@ -251,7 +251,7 @@
    6.22    end
    6.23  
    6.24  fun is_executable_term thy t = can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) (Quickcheck.test_term
    6.25 - (ProofContext.init thy) false (SOME "SML") 1 0)) (preprocess thy [] t)
    6.26 + (ProofContext.init_global thy) false (SOME "SML") 1 0)) (preprocess thy [] t)
    6.27  fun is_executable_thm thy th = is_executable_term thy (prop_of th)
    6.28  
    6.29  val freezeT =
     7.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon May 03 07:59:51 2010 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon May 03 14:25:56 2010 +0200
     7.3 @@ -151,7 +151,7 @@
     7.4  val meta_spec = thm "meta_spec";
     7.5  
     7.6  fun projections rule =
     7.7 -  Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
     7.8 +  Project_Rule.projections (ProofContext.init_global (Thm.theory_of_thm rule)) rule
     7.9    |> map (Drule.export_without_context #> Rule_Cases.save rule);
    7.10  
    7.11  val supp_prod = thm "supp_prod";
    7.12 @@ -1617,7 +1617,7 @@
    7.13              val y = Free ("y", U);
    7.14              val y' = Free ("y'", U)
    7.15            in
    7.16 -            Drule.export_without_context (Goal.prove (ProofContext.init thy11) []
    7.17 +            Drule.export_without_context (Goal.prove (ProofContext.init_global thy11) []
    7.18                (map (augment_sort thy11 fs_cp_sort)
    7.19                  (finite_prems @
    7.20                     [HOLogic.mk_Trueprop (R $ x $ y),
    7.21 @@ -1712,7 +1712,7 @@
    7.22             (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
    7.23  
    7.24      val rec_unique_thms = split_conj_thm (Goal.prove
    7.25 -      (ProofContext.init thy11) (map fst rec_unique_frees)
    7.26 +      (ProofContext.init_global thy11) (map fst rec_unique_frees)
    7.27        (map (augment_sort thy11 fs_cp_sort)
    7.28          (flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
    7.29        (augment_sort thy11 fs_cp_sort
     8.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 03 07:59:51 2010 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 03 14:25:56 2010 +0200
     8.3 @@ -124,7 +124,7 @@
     8.4    (* Find the variable we instantiate *)
     8.5    let
     8.6      val thy = theory_of_thm thm;
     8.7 -    val ctxt = ProofContext.init thy;
     8.8 +    val ctxt = ProofContext.init_global thy;
     8.9      val ss = global_simpset_of thy;
    8.10      val abs_fresh = PureThy.get_thms thy "abs_fresh";
    8.11      val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
     9.1 --- a/src/HOL/Statespace/state_space.ML	Mon May 03 07:59:51 2010 +0200
     9.2 +++ b/src/HOL/Statespace/state_space.ML	Mon May 03 14:25:56 2010 +0200
     9.3 @@ -440,7 +440,7 @@
     9.4  
     9.5     fun string_of_typ T =
     9.6        setmp_CRITICAL show_sorts true
     9.7 -       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
     9.8 +       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
     9.9     val fixestate = (case state_type of
    9.10           NONE => []
    9.11         | SOME s =>
    9.12 @@ -502,7 +502,7 @@
    9.13        *)
    9.14      val _ = writeln ("Defining statespace " ^ quote name ^ " ...");
    9.15  
    9.16 -    val ctxt = ProofContext.init thy;
    9.17 +    val ctxt = ProofContext.init_global thy;
    9.18  
    9.19      fun add_parent (Ts,pname,rs) env =
    9.20        let
    10.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon May 03 07:59:51 2010 +0200
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon May 03 14:25:56 2010 +0200
    10.3 @@ -100,7 +100,7 @@
    10.4          val def' = Syntax.check_term lthy def;
    10.5          val ((_, (_, thm)), lthy') = Specification.definition
    10.6            (NONE, (Attrib.empty_binding, def')) lthy;
    10.7 -        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
    10.8 +        val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
    10.9          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   10.10        in (thm', lthy') end;
   10.11      fun tac thms = Class.intro_classes_tac []
    11.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 03 07:59:51 2010 +0200
    11.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 03 14:25:56 2010 +0200
    11.3 @@ -165,7 +165,7 @@
    11.4  
    11.5  fun read_typ thy str sorts =
    11.6    let
    11.7 -    val ctxt = ProofContext.init thy
    11.8 +    val ctxt = ProofContext.init_global thy
    11.9        |> fold (Variable.declare_typ o TFree) sorts;
   11.10      val T = Syntax.read_typ ctxt str;
   11.11    in (T, Term.add_tfreesT T sorts) end;
   11.12 @@ -316,7 +316,7 @@
   11.13      val (splits, thy9) = Datatype_Abs_Proofs.prove_split_thms
   11.14        config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
   11.15  
   11.16 -    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
   11.17 +    val inducts = Project_Rule.projections (ProofContext.init_global thy2) induct;
   11.18      val dt_infos = map_index
   11.19        (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
   11.20        (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
   11.21 @@ -435,7 +435,7 @@
   11.22        end;
   11.23    in
   11.24      thy
   11.25 -    |> ProofContext.init
   11.26 +    |> ProofContext.init_global
   11.27      |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
   11.28    end;
   11.29  
    12.1 --- a/src/HOL/Tools/Function/size.ML	Mon May 03 07:59:51 2010 +0200
    12.2 +++ b/src/HOL/Tools/Function/size.ML	Mon May 03 14:25:56 2010 +0200
    12.3 @@ -133,7 +133,7 @@
    12.4          val (thm, lthy') = lthy
    12.5            |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
    12.6            |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
    12.7 -        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
    12.8 +        val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy');
    12.9          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   12.10        in (thm', lthy') end;
   12.11  
   12.12 @@ -152,7 +152,7 @@
   12.13        ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   12.14        ||> Local_Theory.exit_global;
   12.15  
   12.16 -    val ctxt = ProofContext.init thy';
   12.17 +    val ctxt = ProofContext.init_global thy';
   12.18  
   12.19      val simpset1 = HOL_basic_ss addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
   12.20        size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 03 07:59:51 2010 +0200
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 03 14:25:56 2010 +0200
    13.3 @@ -286,7 +286,7 @@
    13.4    end
    13.5  
    13.6  fun default_params thy =
    13.7 -  extract_params (ProofContext.init thy) false (default_raw_params thy)
    13.8 +  extract_params (ProofContext.init_global thy) false (default_raw_params thy)
    13.9    o map (apsnd single)
   13.10  
   13.11  val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
    14.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon May 03 07:59:51 2010 +0200
    14.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon May 03 14:25:56 2010 +0200
    14.3 @@ -778,7 +778,7 @@
    14.4        let
    14.5          val (_, args) = strip_comb atom
    14.6        in rewrite_args args end
    14.7 -    val ctxt = ProofContext.init thy
    14.8 +    val ctxt = ProofContext.init_global thy
    14.9      val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
   14.10      val intro_t = prop_of intro'
   14.11      val concl = Logic.strip_imp_concl intro_t
   14.12 @@ -860,7 +860,8 @@
   14.13  
   14.14  fun peephole_optimisation thy intro =
   14.15    let
   14.16 -    val process = MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init thy))
   14.17 +    val process =
   14.18 +      MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy))
   14.19      fun process_False intro_t =
   14.20        if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
   14.21      fun process_True intro_t =
    15.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon May 03 07:59:51 2010 +0200
    15.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon May 03 14:25:56 2010 +0200
    15.3 @@ -580,7 +580,7 @@
    15.4      fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
    15.5         HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
    15.6       | replace_eqs t = t
    15.7 -    val ctxt = ProofContext.init thy
    15.8 +    val ctxt = ProofContext.init_global thy
    15.9      val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
   15.10      val prems = Thm.prems_of elimrule
   15.11      val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
   15.12 @@ -608,7 +608,7 @@
   15.13  val no_compilation = ([], ([], []))
   15.14  
   15.15  fun fetch_pred_data thy name =
   15.16 -  case try (Inductive.the_inductive (ProofContext.init thy)) name of
   15.17 +  case try (Inductive.the_inductive (ProofContext.init_global thy)) name of
   15.18      SOME (info as (_, result)) => 
   15.19        let
   15.20          fun is_intro_of intro =
   15.21 @@ -621,7 +621,7 @@
   15.22          val pre_elim = nth (#elims result) index
   15.23          val pred = nth (#preds result) index
   15.24          val nparams = length (Inductive.params_of (#raw_induct result))
   15.25 -        val ctxt = ProofContext.init thy
   15.26 +        val ctxt = ProofContext.init_global thy
   15.27          val elim_t = mk_casesrule ctxt pred intros
   15.28          val elim =
   15.29            prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
   15.30 @@ -636,7 +636,7 @@
   15.31    in PredData.map (Graph.map_node name (map_pred_data add)) end
   15.32  
   15.33  fun is_inductive_predicate thy name =
   15.34 -  is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
   15.35 +  is_some (try (Inductive.the_inductive (ProofContext.init_global thy)) name)
   15.36  
   15.37  fun depending_preds_of thy (key, value) =
   15.38    let
   15.39 @@ -688,7 +688,7 @@
   15.40      val pred = Const (constname, T)
   15.41      val pre_elim = 
   15.42        (Drule.export_without_context o Skip_Proof.make_thm thy)
   15.43 -      (mk_casesrule (ProofContext.init thy) pred pre_intros)
   15.44 +      (mk_casesrule (ProofContext.init_global thy) pred pre_intros)
   15.45    in register_predicate (constname, pre_intros, pre_elim) thy end
   15.46  
   15.47  fun defined_function_of compilation pred =
   15.48 @@ -1160,7 +1160,7 @@
   15.49  fun is_possible_output thy vs t =
   15.50    forall
   15.51      (fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
   15.52 -      (non_invertible_subterms (ProofContext.init thy) t)
   15.53 +      (non_invertible_subterms (ProofContext.init_global thy) t)
   15.54    andalso
   15.55      (forall (is_eqT o snd)
   15.56        (inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
   15.57 @@ -1367,7 +1367,7 @@
   15.58            val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
   15.59          in (modes, modes) end
   15.60      val (in_ts, out_ts) = split_mode mode ts
   15.61 -    val in_vs = maps (vars_of_destructable_term (ProofContext.init thy)) in_ts
   15.62 +    val in_vs = maps (vars_of_destructable_term (ProofContext.init_global thy)) in_ts
   15.63      val out_vs = terms_vs out_ts
   15.64      fun known_vs_after p vs = (case p of
   15.65          Prem t => union (op =) vs (term_vs t)
   15.66 @@ -1939,7 +1939,7 @@
   15.67  
   15.68  fun compile_pred options compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
   15.69    let
   15.70 -    val ctxt = ProofContext.init thy
   15.71 +    val ctxt = ProofContext.init_global thy
   15.72      val compilation_modifiers = if pol then compilation_modifiers else
   15.73        negative_comp_modifiers_of compilation_modifiers
   15.74      val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
   15.75 @@ -2072,11 +2072,11 @@
   15.76      val simprules = [defthm, @{thm eval_pred},
   15.77        @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   15.78      val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
   15.79 -    val introthm = Goal.prove (ProofContext.init thy)
   15.80 +    val introthm = Goal.prove (ProofContext.init_global thy)
   15.81        (argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
   15.82      val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   15.83      val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
   15.84 -    val elimthm = Goal.prove (ProofContext.init thy)
   15.85 +    val elimthm = Goal.prove (ProofContext.init_global thy)
   15.86        (argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
   15.87      val opt_neg_introthm =
   15.88        if is_all_input mode then
   15.89 @@ -2090,7 +2090,7 @@
   15.90              Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps
   15.91                (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
   15.92              THEN rtac @{thm Predicate.singleI} 1
   15.93 -        in SOME (Goal.prove (ProofContext.init thy) (argnames @ hoarg_names') []
   15.94 +        in SOME (Goal.prove (ProofContext.init_global thy) (argnames @ hoarg_names') []
   15.95              neg_introtrm (fn _ => tac))
   15.96          end
   15.97        else NONE
   15.98 @@ -2604,7 +2604,7 @@
   15.99  
  15.100  fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) =
  15.101    let
  15.102 -    val ctxt = ProofContext.init thy
  15.103 +    val ctxt = ProofContext.init_global thy
  15.104      val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
  15.105    in
  15.106      Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
  15.107 @@ -2667,7 +2667,7 @@
  15.108      val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
  15.109      val (preds, intrs) = unify_consts thy preds intrs
  15.110      val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs]
  15.111 -      (ProofContext.init thy)
  15.112 +      (ProofContext.init_global thy)
  15.113      val preds = map dest_Const preds
  15.114      val all_vs = terms_vs intrs
  15.115      val all_modes = 
  15.116 @@ -2744,7 +2744,7 @@
  15.117          val nparams = nparams_of thy predname
  15.118          val elim' =
  15.119            (Drule.export_without_context o Skip_Proof.make_thm thy)
  15.120 -          (mk_casesrule (ProofContext.init thy) nparams intros)
  15.121 +          (mk_casesrule (ProofContext.init_global thy) nparams intros)
  15.122        in
  15.123          if not (Thm.equiv_thm (elim, elim')) then
  15.124            error "Introduction and elimination rules do not match!"
  15.125 @@ -2757,7 +2757,7 @@
  15.126  
  15.127  fun add_code_equations thy preds result_thmss =
  15.128    let
  15.129 -    val ctxt = ProofContext.init thy
  15.130 +    val ctxt = ProofContext.init_global thy
  15.131      fun add_code_equation (predname, T) (pred, result_thms) =
  15.132        let
  15.133          val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
  15.134 @@ -3047,7 +3047,7 @@
  15.135      fun after_qed thms goal_ctxt =
  15.136        let
  15.137          val global_thms = ProofContext.export goal_ctxt
  15.138 -          (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
  15.139 +          (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms)
  15.140        in
  15.141          goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #>
  15.142            ((case compilation options of
  15.143 @@ -3164,7 +3164,7 @@
  15.144            | DSeq => dseq_comp_modifiers
  15.145            | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
  15.146            | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
  15.147 -        val t_pred = compile_expr comp_modifiers (ProofContext.init thy)
  15.148 +        val t_pred = compile_expr comp_modifiers (ProofContext.init_global thy)
  15.149            (body, deriv) additional_arguments;
  15.150          val T_pred = dest_predT compfuns (fastype_of t_pred)
  15.151          val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
    16.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon May 03 07:59:51 2010 +0200
    16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Mon May 03 14:25:56 2010 +0200
    16.3 @@ -129,7 +129,7 @@
    16.4    
    16.5  fun split_all_pairs thy th =
    16.6    let
    16.7 -    val ctxt = ProofContext.init thy
    16.8 +    val ctxt = ProofContext.init_global thy
    16.9      val ((_, [th']), ctxt') = Variable.import true [th] ctxt
   16.10      val t = prop_of th'
   16.11      val frees = Term.add_frees t [] 
   16.12 @@ -153,7 +153,7 @@
   16.13  
   16.14  fun inline_equations thy th =
   16.15    let
   16.16 -    val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init thy)
   16.17 +    val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init_global thy)
   16.18      val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th
   16.19      (*val _ = print_step options 
   16.20        ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
   16.21 @@ -188,7 +188,7 @@
   16.22          tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
   16.23            " with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
   16.24        else ()
   16.25 -    val ctxt = ProofContext.init thy
   16.26 +    val ctxt = ProofContext.init_global thy
   16.27      fun filtering th =
   16.28        if is_equationlike th andalso
   16.29          defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
    17.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon May 03 07:59:51 2010 +0200
    17.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon May 03 14:25:56 2010 +0200
    17.3 @@ -195,7 +195,7 @@
    17.4            SOME raw_split_thm =>
    17.5            let
    17.6              val (f, args) = strip_comb t
    17.7 -            val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
    17.8 +            val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
    17.9              val (assms, concl) = Logic.strip_horn (prop_of split_thm)
   17.10              val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
   17.11              val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
    18.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon May 03 07:59:51 2010 +0200
    18.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon May 03 14:25:56 2010 +0200
    18.3 @@ -64,7 +64,7 @@
    18.4  fun instantiated_case_rewrites thy Tcon =
    18.5    let
    18.6      val rew_ths = case_rewrites thy Tcon
    18.7 -    val ctxt = ProofContext.init thy
    18.8 +    val ctxt = ProofContext.init_global thy
    18.9      fun instantiate th =
   18.10      let
   18.11        val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
   18.12 @@ -128,9 +128,10 @@
   18.13        | SOME raw_split_thm =>
   18.14          let
   18.15            val (f, args) = strip_comb atom
   18.16 -          val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
   18.17 +          val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
   18.18            (* TODO: contextify things - this line is to unvarify the split_thm *)
   18.19 -          (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
   18.20 +          (*val ((_, [isplit_thm]), _) =
   18.21 +            Variable.import true [split_thm] (ProofContext.init_global thy)*)
   18.22            val (assms, concl) = Logic.strip_horn (prop_of split_thm)
   18.23            val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
   18.24            val Tcons = datatype_names_of_case_name thy (fst (dest_Const f))
   18.25 @@ -188,7 +189,7 @@
   18.26  
   18.27  fun flatten_intros constname intros thy =
   18.28    let
   18.29 -    val ctxt = ProofContext.init thy
   18.30 +    val ctxt = ProofContext.init_global thy
   18.31      val ((_, intros), ctxt') = Variable.import true intros ctxt
   18.32      val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
   18.33        (flatten constname) (map prop_of intros) ([], thy)
   18.34 @@ -206,7 +207,7 @@
   18.35  
   18.36  fun introrulify thy ths = 
   18.37    let
   18.38 -    val ctxt = ProofContext.init thy
   18.39 +    val ctxt = ProofContext.init_global thy
   18.40      val ((_, ths'), ctxt') = Variable.import true ths ctxt
   18.41      fun introrulify' th =
   18.42        let
   18.43 @@ -277,7 +278,7 @@
   18.44      SOME specss => (specss, thy)
   18.45    | NONE =>*)
   18.46      let
   18.47 -      val ctxt = ProofContext.init thy
   18.48 +      val ctxt = ProofContext.init_global thy
   18.49        val intros =
   18.50          if forall is_pred_equation specs then 
   18.51            map (map_term thy (maps_premises (split_conjs thy))) (introrulify thy (map rewrite specs))
    19.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon May 03 07:59:51 2010 +0200
    19.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon May 03 14:25:56 2010 +0200
    19.3 @@ -200,7 +200,7 @@
    19.4        (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    19.5         HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
    19.6      val tac = fn _ => Skip_Proof.cheat_tac thy1
    19.7 -    val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac
    19.8 +    val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac
    19.9      val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
   19.10      val (thy3, preproc_time) = cpu_time "predicate preprocessing"
   19.11          (fn () => Predicate_Compile.preprocess options const thy2)
    20.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon May 03 07:59:51 2010 +0200
    20.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon May 03 14:25:56 2010 +0200
    20.3 @@ -65,7 +65,7 @@
    20.4  
    20.5  fun specialise_intros black_list (pred, intros) pats thy =
    20.6    let
    20.7 -    val ctxt = ProofContext.init thy
    20.8 +    val ctxt = ProofContext.init_global thy
    20.9      val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
   20.10      val pats = map (Logic.incr_indexes ([],  maxidx + 1)) pats
   20.11      val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
    21.1 --- a/src/HOL/Tools/TFL/post.ML	Mon May 03 07:59:51 2010 +0200
    21.2 +++ b/src/HOL/Tools/TFL/post.ML	Mon May 03 14:25:56 2010 +0200
    21.3 @@ -140,7 +140,7 @@
    21.4  
    21.5  fun simplify_defn strict thy cs ss congs wfs id pats def0 =
    21.6     let
    21.7 -       val ctxt = ProofContext.init thy
    21.8 +       val ctxt = ProofContext.init_global thy
    21.9         val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
   21.10         val {rules,rows,TCs,full_pats_TCs} =
   21.11             Prim.post_definition congs (thy, (def,pats))
    22.1 --- a/src/HOL/Tools/TFL/rules.ML	Mon May 03 07:59:51 2010 +0200
    22.2 +++ b/src/HOL/Tools/TFL/rules.ML	Mon May 03 14:25:56 2010 +0200
    22.3 @@ -814,7 +814,7 @@
    22.4    let
    22.5      val thy = Thm.theory_of_cterm ptm;
    22.6      val t = Thm.term_of ptm;
    22.7 -    val ctxt = ProofContext.init thy |> Variable.auto_fixes t;
    22.8 +    val ctxt = ProofContext.init_global thy |> Variable.auto_fixes t;
    22.9    in
   22.10      if strict then Goal.prove ctxt [] [] t (K tac)
   22.11      else Goal.prove ctxt [] [] t (K tac)
    23.1 --- a/src/HOL/Tools/TFL/tfl.ML	Mon May 03 07:59:51 2010 +0200
    23.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Mon May 03 14:25:56 2010 +0200
    23.3 @@ -361,7 +361,7 @@
    23.4  
    23.5  (*For Isabelle, the lhs of a definition must be a constant.*)
    23.6  fun const_def sign (c, Ty, rhs) =
    23.7 -  singleton (Syntax.check_terms (ProofContext.init sign))
    23.8 +  singleton (Syntax.check_terms (ProofContext.init_global sign))
    23.9      (Const("==",dummyT) $ Const(c,Ty) $ rhs);
   23.10  
   23.11  (*Make all TVars available for instantiation by adding a ? to the front*)
    24.1 --- a/src/HOL/Tools/choice_specification.ML	Mon May 03 07:59:51 2010 +0200
    24.2 +++ b/src/HOL/Tools/choice_specification.ML	Mon May 03 14:25:56 2010 +0200
    24.3 @@ -225,7 +225,7 @@
    24.4          #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
    24.5      in
    24.6        thy
    24.7 -      |> ProofContext.init
    24.8 +      |> ProofContext.init_global
    24.9        |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
   24.10      end;
   24.11  
    25.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon May 03 07:59:51 2010 +0200
    25.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon May 03 14:25:56 2010 +0200
    25.3 @@ -66,7 +66,7 @@
    25.4            val nparms = (case optnparms of
    25.5              SOME k => k
    25.6            | NONE => (case rules of
    25.7 -             [] => (case try (Inductive.the_inductive (ProofContext.init thy)) s of
    25.8 +             [] => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
    25.9                   SOME (_, {raw_induct, ...}) =>
   25.10                     length (Inductive.params_of raw_induct)
   25.11                 | NONE => 0)
   25.12 @@ -84,7 +84,7 @@
   25.13  fun get_clauses thy s =
   25.14    let val {intros, graph, ...} = CodegenData.get thy
   25.15    in case Symtab.lookup intros s of
   25.16 -      NONE => (case try (Inductive.the_inductive (ProofContext.init thy)) s of
   25.17 +      NONE => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
   25.18          NONE => NONE
   25.19        | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
   25.20            SOME (names, Codegen.thyname_of_const thy s,
    26.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon May 03 07:59:51 2010 +0200
    26.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon May 03 14:25:56 2010 +0200
    26.3 @@ -137,7 +137,7 @@
    26.4  
    26.5  fun fun_of_prem thy rsets vs params rule ivs intr =
    26.6    let
    26.7 -    val ctxt = ProofContext.init thy
    26.8 +    val ctxt = ProofContext.init_global thy
    26.9      val args = map (Free o apfst fst o dest_Var) ivs;
   26.10      val args' = map (Free o apfst fst)
   26.11        (subtract (op =) params (Term.add_vars (prop_of intr) []));
   26.12 @@ -484,7 +484,7 @@
   26.13  fun add_ind_realizers name rsets thy =
   26.14    let
   26.15      val (_, {intrs, induct, raw_induct, elims, ...}) =
   26.16 -      Inductive.the_inductive (ProofContext.init thy) name;
   26.17 +      Inductive.the_inductive (ProofContext.init_global thy) name;
   26.18      val vss = sort (int_ord o pairself length)
   26.19        (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
   26.20    in
    27.1 --- a/src/HOL/Tools/old_primrec.ML	Mon May 03 07:59:51 2010 +0200
    27.2 +++ b/src/HOL/Tools/old_primrec.ML	Mon May 03 14:25:56 2010 +0200
    27.3 @@ -214,7 +214,7 @@
    27.4                                  fs @ map Bound (0 ::(length ls downto 1))))
    27.5      val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def";
    27.6      val def_prop =
    27.7 -      singleton (Syntax.check_terms (ProofContext.init thy))
    27.8 +      singleton (Syntax.check_terms (ProofContext.init_global thy))
    27.9          (Logic.mk_equals (Const (fname, dummyT), rhs));
   27.10    in (def_name, def_prop) end;
   27.11  
    28.1 --- a/src/HOL/Tools/recdef.ML	Mon May 03 07:59:51 2010 +0200
    28.2 +++ b/src/HOL/Tools/recdef.ML	Mon May 03 14:25:56 2010 +0200
    28.3 @@ -160,7 +160,7 @@
    28.4  
    28.5  fun prepare_hints thy opt_src =
    28.6    let
    28.7 -    val ctxt0 = ProofContext.init thy;
    28.8 +    val ctxt0 = ProofContext.init_global thy;
    28.9      val ctxt =
   28.10        (case opt_src of
   28.11          NONE => ctxt0
   28.12 @@ -172,7 +172,7 @@
   28.13  
   28.14  fun prepare_hints_i thy () =
   28.15    let
   28.16 -    val ctxt0 = ProofContext.init thy;
   28.17 +    val ctxt0 = ProofContext.init_global thy;
   28.18      val {simps, congs, wfs} = get_global_hints thy;
   28.19    in (claset_of ctxt0, simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
   28.20  
   28.21 @@ -234,7 +234,7 @@
   28.22      val _ = requires_recdef thy;
   28.23      val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
   28.24  
   28.25 -    val congs = eval_thms (ProofContext.init thy) raw_congs;
   28.26 +    val congs = eval_thms (ProofContext.init_global thy) raw_congs;
   28.27      val (thy2, induct_rules) = tfl_fn thy congs name eqs;
   28.28      val ([induct_rules'], thy3) =
   28.29        thy2
    29.1 --- a/src/HOL/Tools/record.ML	Mon May 03 07:59:51 2010 +0200
    29.2 +++ b/src/HOL/Tools/record.ML	Mon May 03 14:25:56 2010 +0200
    29.3 @@ -1038,7 +1038,7 @@
    29.4    let val thm =
    29.5      if ! quick_and_dirty then Skip_Proof.make_thm thy prop
    29.6      else if Goal.future_enabled () then
    29.7 -      Goal.future_result (ProofContext.init thy) (Future.fork_pri ~1 prf) prop
    29.8 +      Goal.future_result (ProofContext.init_global thy) (Future.fork_pri ~1 prf) prop
    29.9      else prf ()
   29.10    in Drule.export_without_context thm end;
   29.11  
   29.12 @@ -1048,7 +1048,7 @@
   29.13        if ! quick_and_dirty then Skip_Proof.prove
   29.14        else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
   29.15        else Goal.prove_future;
   29.16 -    val prf = prv (ProofContext.init thy) [] asms prop tac;
   29.17 +    val prf = prv (ProofContext.init_global thy) [] asms prop tac;
   29.18    in if stndrd then Drule.export_without_context prf else prf end;
   29.19  
   29.20  val prove_future_global = prove_common false;
   29.21 @@ -1090,7 +1090,7 @@
   29.22            else mk_comp_id acc;
   29.23          val prop = lhs === rhs;
   29.24          val othm =
   29.25 -          Goal.prove (ProofContext.init thy) [] [] prop
   29.26 +          Goal.prove (ProofContext.init_global thy) [] [] prop
   29.27              (fn _ =>
   29.28                simp_tac defset 1 THEN
   29.29                REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   29.30 @@ -1114,7 +1114,7 @@
   29.31        else mk_comp (u' $ f') (u $ f);
   29.32      val prop = lhs === rhs;
   29.33      val othm =
   29.34 -      Goal.prove (ProofContext.init thy) [] [] prop
   29.35 +      Goal.prove (ProofContext.init_global thy) [] [] prop
   29.36          (fn _ =>
   29.37            simp_tac defset 1 THEN
   29.38            REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   29.39 @@ -1155,7 +1155,7 @@
   29.40      val (_, args) = strip_comb lhs;
   29.41      val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
   29.42    in
   29.43 -    Goal.prove (ProofContext.init thy) [] [] prop'
   29.44 +    Goal.prove (ProofContext.init_global thy) [] [] prop'
   29.45        (fn _ =>
   29.46          simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
   29.47          TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
   29.48 @@ -1247,7 +1247,7 @@
   29.49      val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)];
   29.50      val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
   29.51    in
   29.52 -    Goal.prove (ProofContext.init thy) [] [] prop
   29.53 +    Goal.prove (ProofContext.init_global thy) [] [] prop
   29.54        (fn _ =>
   29.55          simp_tac simpset 1 THEN
   29.56          REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   29.57 @@ -2388,7 +2388,7 @@
   29.58        if quiet_mode then ()
   29.59        else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
   29.60  
   29.61 -    val ctxt = ProofContext.init thy;
   29.62 +    val ctxt = ProofContext.init_global thy;
   29.63      fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T)
   29.64        handle TYPE (msg, _, _) => error msg;
   29.65  
   29.66 @@ -2438,7 +2438,7 @@
   29.67  
   29.68  fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
   29.69    let
   29.70 -    val ctxt = ProofContext.init thy;
   29.71 +    val ctxt = ProofContext.init_global thy;
   29.72      val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
   29.73      val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
   29.74      val (parent, ctxt2) = read_parent raw_parent ctxt1;
    30.1 --- a/src/HOL/Tools/typecopy.ML	Mon May 03 07:59:51 2010 +0200
    30.2 +++ b/src/HOL/Tools/typecopy.ML	Mon May 03 14:25:56 2010 +0200
    30.3 @@ -52,7 +52,7 @@
    30.4  fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
    30.5    let
    30.6      val ty = Sign.certify_typ thy raw_ty;
    30.7 -    val ctxt = ProofContext.init thy |> Variable.declare_typ ty;
    30.8 +    val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
    30.9      val vs = map (ProofContext.check_tfree ctxt) raw_vs;
   30.10      val tac = Tactic.rtac UNIV_witness 1;
   30.11      fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
    31.1 --- a/src/HOL/Tools/typedef.ML	Mon May 03 07:59:51 2010 +0200
    31.2 +++ b/src/HOL/Tools/typedef.ML	Mon May 03 14:25:56 2010 +0200
    31.3 @@ -182,7 +182,8 @@
    31.4          val thy = ProofContext.theory_of set_lthy;
    31.5          val cert = Thm.cterm_of thy;
    31.6          val (defs, A) =
    31.7 -          Local_Defs.export_cterm set_lthy (ProofContext.init thy) (cert set') ||> Thm.term_of;
    31.8 +          Local_Defs.export_cterm set_lthy (ProofContext.init_global thy) (cert set')
    31.9 +          ||> Thm.term_of;
   31.10  
   31.11          val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
   31.12            Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
    32.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 03 07:59:51 2010 +0200
    32.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 03 14:25:56 2010 +0200
    32.3 @@ -189,7 +189,7 @@
    32.4          (K (beta_tac 1));
    32.5      val tuple_unfold_thm =
    32.6        (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
    32.7 -      |> Local_Defs.unfold (ProofContext.init thy) @{thms split_conv};
    32.8 +      |> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv};
    32.9  
   32.10      fun mk_unfold_thms [] thm = []
   32.11        | mk_unfold_thms (n::[]) thm = [(n, thm)]
   32.12 @@ -380,7 +380,7 @@
   32.13  
   32.14  fun read_typ thy str sorts =
   32.15    let
   32.16 -    val ctxt = ProofContext.init thy
   32.17 +    val ctxt = ProofContext.init_global thy
   32.18        |> fold (Variable.declare_typ o TFree) sorts;
   32.19      val T = Syntax.read_typ ctxt str;
   32.20    in (T, Term.add_tfreesT T sorts) end;
    33.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon May 03 07:59:51 2010 +0200
    33.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon May 03 14:25:56 2010 +0200
    33.3 @@ -71,7 +71,7 @@
    33.4  end;
    33.5  
    33.6  fun legacy_infer_term thy t =
    33.7 -  let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
    33.8 +  let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init_global thy)
    33.9    in singleton (Syntax.check_terms ctxt) (intern_term thy t) end;
   33.10  
   33.11  fun pg'' thy defs t tacs =
   33.12 @@ -347,7 +347,7 @@
   33.13  
   33.14  (* ----- theorems concerning finiteness and induction ----------------------- *)
   33.15  
   33.16 -  val global_ctxt = ProofContext.init thy;
   33.17 +  val global_ctxt = ProofContext.init_global thy;
   33.18  
   33.19    val _ = trace " Proving ind...";
   33.20    val ind =
   33.21 @@ -422,7 +422,7 @@
   33.22            bot :: map (fn (c,_) => Long_Name.base_name c) cons;
   33.23    in adms @ flat (map2 one_eq bottoms eqs) end;
   33.24  
   33.25 -val inducts = Project_Rule.projections (ProofContext.init thy) ind;
   33.26 +val inducts = Project_Rule.projections (ProofContext.init_global thy) ind;
   33.27  fun ind_rule (dname, rule) =
   33.28      ((Binding.empty, [rule]),
   33.29       [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
   33.30 @@ -470,7 +470,7 @@
   33.31  local
   33.32  
   33.33    fun legacy_infer_term thy t =
   33.34 -      singleton (Syntax.check_terms (ProofContext.init thy)) (intern_term thy t);
   33.35 +      singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
   33.36    fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
   33.37    fun infer_props thy = map (apsnd (legacy_infer_prop thy));
   33.38    fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
    34.1 --- a/src/HOLCF/Tools/pcpodef.ML	Mon May 03 07:59:51 2010 +0200
    34.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Mon May 03 14:25:56 2010 +0200
    34.3 @@ -170,7 +170,7 @@
    34.4  
    34.5      (*rhs*)
    34.6      val tmp_ctxt =
    34.7 -      ProofContext.init thy
    34.8 +      ProofContext.init_global thy
    34.9        |> fold (Variable.declare_typ o TFree) raw_args;
   34.10      val set = prep_term tmp_ctxt raw_set;
   34.11      val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
   34.12 @@ -207,7 +207,7 @@
   34.13      val ((_, (_, below_ldef)), lthy4) = lthy3
   34.14        |> Specification.definition (NONE,
   34.15            ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
   34.16 -    val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
   34.17 +    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4);
   34.18      val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef;
   34.19      val thy5 = lthy4
   34.20        |> Class.prove_instantiation_instance
   34.21 @@ -322,7 +322,7 @@
   34.22  fun gen_cpodef_proof prep_term prep_constraint
   34.23      ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
   34.24    let
   34.25 -    val ctxt = ProofContext.init thy;
   34.26 +    val ctxt = ProofContext.init_global thy;
   34.27      val args = map (apsnd (prep_constraint ctxt)) raw_args;
   34.28      val (goal1, goal2, make_result) =
   34.29        prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
   34.30 @@ -333,7 +333,7 @@
   34.31  fun gen_pcpodef_proof prep_term prep_constraint
   34.32      ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
   34.33    let
   34.34 -    val ctxt = ProofContext.init thy;
   34.35 +    val ctxt = ProofContext.init_global thy;
   34.36      val args = map (apsnd (prep_constraint ctxt)) raw_args;
   34.37      val (goal1, goal2, make_result) =
   34.38        prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
    35.1 --- a/src/HOLCF/Tools/repdef.ML	Mon May 03 07:59:51 2010 +0200
    35.2 +++ b/src/HOLCF/Tools/repdef.ML	Mon May 03 14:25:56 2010 +0200
    35.3 @@ -65,7 +65,7 @@
    35.4  
    35.5      (*rhs*)
    35.6      val tmp_ctxt =
    35.7 -      ProofContext.init thy
    35.8 +      ProofContext.init_global thy
    35.9        |> fold (Variable.declare_typ o TFree) raw_args;
   35.10      val defl = prep_term tmp_ctxt raw_defl;
   35.11      val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl;
   35.12 @@ -119,7 +119,7 @@
   35.13          Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
   35.14      val ((_, (_, approx_ldef)), lthy) =
   35.15          Specification.definition (NONE, (approx_bind, approx_eqn)) lthy;
   35.16 -    val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
   35.17 +    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
   35.18      val emb_def = singleton (ProofContext.export lthy ctxt_thy) emb_ldef;
   35.19      val prj_def = singleton (ProofContext.export lthy ctxt_thy) prj_ldef;
   35.20      val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef;
   35.21 @@ -161,7 +161,7 @@
   35.22  
   35.23  fun repdef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy =
   35.24    let
   35.25 -    val ctxt = ProofContext.init thy;
   35.26 +    val ctxt = ProofContext.init_global thy;
   35.27      val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args;
   35.28    in snd (gen_add_repdef Syntax.read_term def name (b, args, mx) A morphs thy) end;
   35.29  
    36.1 --- a/src/Provers/classical.ML	Mon May 03 07:59:51 2010 +0200
    36.2 +++ b/src/Provers/classical.ML	Mon May 03 14:25:56 2010 +0200
    36.3 @@ -210,7 +210,7 @@
    36.4  fun dup_elim th =
    36.5    let
    36.6      val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    36.7 -    val ctxt = ProofContext.init (Thm.theory_of_thm rl);
    36.8 +    val ctxt = ProofContext.init_global (Thm.theory_of_thm rl);
    36.9    in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
   36.10  
   36.11  
   36.12 @@ -856,7 +856,7 @@
   36.13  
   36.14  fun global_claset_of thy =
   36.15    let val (cs, ctxt_cs) = GlobalClaset.get thy
   36.16 -  in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
   36.17 +  in context_cs (ProofContext.init_global thy) cs (ctxt_cs) end;
   36.18  
   36.19  
   36.20  (* context dependent components *)
    37.1 --- a/src/Provers/quantifier1.ML	Mon May 03 07:59:51 2010 +0200
    37.2 +++ b/src/Provers/quantifier1.ML	Mon May 03 14:25:56 2010 +0200
    37.3 @@ -113,7 +113,7 @@
    37.4    in exqu [] end;
    37.5  
    37.6  fun prove_conv tac thy tu =
    37.7 -  Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
    37.8 +  Goal.prove (ProofContext.init_global thy) [] [] (Logic.mk_equals tu)
    37.9      (K (rtac iff_reflection 1 THEN tac));
   37.10  
   37.11  fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
    38.1 --- a/src/Pure/Isar/class.ML	Mon May 03 07:59:51 2010 +0200
    38.2 +++ b/src/Pure/Isar/class.ML	Mon May 03 14:25:56 2010 +0200
    38.3 @@ -32,7 +32,7 @@
    38.4  
    38.5  fun calculate thy class sups base_sort param_map assm_axiom =
    38.6    let
    38.7 -    val empty_ctxt = ProofContext.init thy;
    38.8 +    val empty_ctxt = ProofContext.init_global thy;
    38.9  
   38.10      (* instantiation of canonical interpretation *)
   38.11      val aT = TFree (Name.aT, base_sort);
   38.12 @@ -143,7 +143,7 @@
   38.13        #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
   38.14      val raw_supexpr = (map (fn sup => (sup, (("", false),
   38.15        Expression.Positional []))) sups, []);
   38.16 -    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
   38.17 +    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy
   38.18        |> prep_decl raw_supexpr init_class_body raw_elems;
   38.19      fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
   38.20        | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
   38.21 @@ -194,7 +194,7 @@
   38.22      val sup_sort = inter_sort base_sort sups;
   38.23  
   38.24      (* process elements as class specification *)
   38.25 -    val class_ctxt = begin sups base_sort (ProofContext.init thy);
   38.26 +    val class_ctxt = begin sups base_sort (ProofContext.init_global thy);
   38.27      val ((_, _, syntax_elems), _) = class_ctxt
   38.28        |> Expression.cert_declaration supexpr I inferred_elems;
   38.29      fun check_vars e vs = if null vs
   38.30 @@ -340,7 +340,7 @@
   38.31  
   38.32  val subclass = gen_subclass (K I) user_proof;
   38.33  fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
   38.34 -val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init) user_proof;
   38.35 +val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init_global) user_proof;
   38.36  
   38.37  end; (*local*)
   38.38  
    39.1 --- a/src/Pure/Isar/class_target.ML	Mon May 03 07:59:51 2010 +0200
    39.2 +++ b/src/Pure/Isar/class_target.ML	Mon May 03 14:25:56 2010 +0200
    39.3 @@ -157,7 +157,7 @@
    39.4  
    39.5  fun print_classes thy =
    39.6    let
    39.7 -    val ctxt = ProofContext.init thy;
    39.8 +    val ctxt = ProofContext.init_global thy;
    39.9      val algebra = Sign.classes_of thy;
   39.10      val arities =
   39.11        Symtab.empty
   39.12 @@ -372,7 +372,7 @@
   39.13        ProofContext.theory ((fold o fold) AxClass.add_classrel results);
   39.14    in
   39.15      thy
   39.16 -    |> ProofContext.init
   39.17 +    |> ProofContext.init_global
   39.18      |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
   39.19    end;
   39.20  
   39.21 @@ -421,7 +421,7 @@
   39.22  
   39.23  fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
   39.24    let
   39.25 -    val ctxt = ProofContext.init thy;
   39.26 +    val ctxt = ProofContext.init_global thy;
   39.27      val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
   39.28        (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
   39.29      val tycos = map #1 all_arities;
   39.30 @@ -514,7 +514,7 @@
   39.31    in
   39.32      thy
   39.33      |> Theory.checkpoint
   39.34 -    |> ProofContext.init
   39.35 +    |> ProofContext.init_global
   39.36      |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
   39.37      |> fold (Variable.declare_typ o TFree) vs
   39.38      |> fold (Variable.declare_names o Free o snd) params
   39.39 @@ -554,7 +554,7 @@
   39.40  fun prove_instantiation_exit_result f tac x lthy =
   39.41    let
   39.42      val morph = ProofContext.export_morphism lthy
   39.43 -      (ProofContext.init (ProofContext.theory_of lthy));
   39.44 +      (ProofContext.init_global (ProofContext.theory_of lthy));
   39.45      val y = f morph x;
   39.46    in
   39.47      lthy
   39.48 @@ -597,7 +597,7 @@
   39.49        ((fold o fold) AxClass.add_arity results);
   39.50    in
   39.51      thy
   39.52 -    |> ProofContext.init
   39.53 +    |> ProofContext.init_global
   39.54      |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   39.55    end;
   39.56  
    40.1 --- a/src/Pure/Isar/code.ML	Mon May 03 07:59:51 2010 +0200
    40.2 +++ b/src/Pure/Isar/code.ML	Mon May 03 14:25:56 2010 +0200
    40.3 @@ -337,7 +337,7 @@
    40.4  fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
    40.5  
    40.6  fun read_signature thy = cert_signature thy o Type.strip_sorts
    40.7 -  o Syntax.parse_typ (ProofContext.init thy);
    40.8 +  o Syntax.parse_typ (ProofContext.init_global thy);
    40.9  
   40.10  fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
   40.11  
   40.12 @@ -554,7 +554,7 @@
   40.13  
   40.14  fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
   40.15  
   40.16 -fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init thy);
   40.17 +fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy);
   40.18  
   40.19  fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
   40.20    apfst (meta_rewrite thy);
   40.21 @@ -941,7 +941,7 @@
   40.22  
   40.23  fun print_codesetup thy =
   40.24    let
   40.25 -    val ctxt = ProofContext.init thy;
   40.26 +    val ctxt = ProofContext.init_global thy;
   40.27      val exec = the_exec thy;
   40.28      fun pretty_equations const thms =
   40.29        (Pretty.block o Pretty.fbreaks) (
    41.1 --- a/src/Pure/Isar/constdefs.ML	Mon May 03 07:59:51 2010 +0200
    41.2 +++ b/src/Pure/Isar/constdefs.ML	Mon May 03 14:25:56 2010 +0200
    41.3 @@ -26,7 +26,7 @@
    41.4  
    41.5      fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
    41.6  
    41.7 -    val thy_ctxt = ProofContext.init thy;
    41.8 +    val thy_ctxt = ProofContext.init_global thy;
    41.9      val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
   41.10      val ((d, mx), var_ctxt) =
   41.11        (case raw_decl of
   41.12 @@ -62,7 +62,7 @@
   41.13  
   41.14  fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
   41.15    let
   41.16 -    val ctxt = ProofContext.init thy;
   41.17 +    val ctxt = ProofContext.init_global thy;
   41.18      val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
   41.19      val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
   41.20    in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
    42.1 --- a/src/Pure/Isar/expression.ML	Mon May 03 07:59:51 2010 +0200
    42.2 +++ b/src/Pure/Isar/expression.ML	Mon May 03 14:25:56 2010 +0200
    42.3 @@ -642,7 +642,7 @@
    42.4        |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
    42.5        |> PureThy.add_defs false
    42.6          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
    42.7 -    val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
    42.8 +    val defs_ctxt = ProofContext.init_global defs_thy |> Variable.declare_term head;
    42.9  
   42.10      val cert = Thm.cterm_of defs_thy;
   42.11  
   42.12 @@ -729,7 +729,7 @@
   42.13        error ("Duplicate definition of locale " ^ quote name);
   42.14  
   42.15      val ((fixed, deps, body_elems), (parms, ctxt')) =
   42.16 -      prep_decl raw_import I raw_body (ProofContext.init thy);
   42.17 +      prep_decl raw_import I raw_body (ProofContext.init_global thy);
   42.18      val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
   42.19  
   42.20      val predicate_binding =
   42.21 @@ -795,7 +795,7 @@
   42.22  fun gen_interpretation prep_expr parse_prop prep_attr
   42.23      expression equations theory =
   42.24    let
   42.25 -    val ((propss, deps, export), expr_ctxt) = ProofContext.init theory
   42.26 +    val ((propss, deps, export), expr_ctxt) = ProofContext.init_global theory
   42.27        |> prep_expr expression;
   42.28  
   42.29      val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
   42.30 @@ -809,7 +809,8 @@
   42.31          val eqn_attrss = map2 (fn attrs => fn eqn =>
   42.32            ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
   42.33          fun meta_rewrite thy =
   42.34 -          map (Local_Defs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def) o maps snd;
   42.35 +          map (Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) #> Drule.abs_def) o
   42.36 +            maps snd;
   42.37        in
   42.38          thy
   42.39          |> PureThy.note_thmss Thm.lemmaK eqn_attrss
    43.1 --- a/src/Pure/Isar/local_theory.ML	Mon May 03 07:59:51 2010 +0200
    43.2 +++ b/src/Pure/Isar/local_theory.ML	Mon May 03 14:25:56 2010 +0200
    43.3 @@ -181,7 +181,8 @@
    43.4    Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
    43.5  
    43.6  fun target_morphism lthy = standard_morphism lthy (target_of lthy);
    43.7 -fun global_morphism lthy = standard_morphism lthy (ProofContext.init (ProofContext.theory_of lthy));
    43.8 +fun global_morphism lthy =
    43.9 +  standard_morphism lthy (ProofContext.init_global (ProofContext.theory_of lthy));
   43.10  
   43.11  
   43.12  (* primitive operations *)
   43.13 @@ -270,7 +271,7 @@
   43.14  fun exit_result_global f (x, lthy) =
   43.15    let
   43.16      val thy = exit_global lthy;
   43.17 -    val thy_ctxt = ProofContext.init thy;
   43.18 +    val thy_ctxt = ProofContext.init_global thy;
   43.19      val phi = standard_morphism lthy thy_ctxt;
   43.20    in (f phi x, thy) end;
   43.21  
    44.1 --- a/src/Pure/Isar/locale.ML	Mon May 03 07:59:51 2010 +0200
    44.2 +++ b/src/Pure/Isar/locale.ML	Mon May 03 14:25:56 2010 +0200
    44.3 @@ -308,7 +308,7 @@
    44.4  
    44.5  fun init name thy =
    44.6    activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
    44.7 -    ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
    44.8 +    ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
    44.9  
   44.10  fun print_locale thy show_facts raw_name =
   44.11    let
   44.12 @@ -412,7 +412,7 @@
   44.13    let
   44.14      val name = intern thy raw_name;
   44.15      val name' = extern thy name;
   44.16 -    val ctxt = ProofContext.init thy;
   44.17 +    val ctxt = ProofContext.init_global thy;
   44.18      fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
   44.19      fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
   44.20      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
    45.1 --- a/src/Pure/Isar/object_logic.ML	Mon May 03 07:59:51 2010 +0200
    45.2 +++ b/src/Pure/Isar/object_logic.ML	Mon May 03 14:25:56 2010 +0200
    45.3 @@ -186,7 +186,7 @@
    45.4  fun atomize_prems ct =
    45.5    if Logic.has_meta_prems (Thm.term_of ct) then
    45.6      Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize))
    45.7 -      (ProofContext.init (Thm.theory_of_cterm ct)) ct
    45.8 +      (ProofContext.init_global (Thm.theory_of_cterm ct)) ct
    45.9    else Conv.all_conv ct;
   45.10  
   45.11  val atomize_prems_tac = CONVERSION atomize_prems;
    46.1 --- a/src/Pure/Isar/overloading.ML	Mon May 03 07:59:51 2010 +0200
    46.2 +++ b/src/Pure/Isar/overloading.ML	Mon May 03 14:25:56 2010 +0200
    46.3 @@ -156,7 +156,7 @@
    46.4    in
    46.5      thy
    46.6      |> Theory.checkpoint
    46.7 -    |> ProofContext.init
    46.8 +    |> ProofContext.init_global
    46.9      |> OverloadingData.put overloading
   46.10      |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
   46.11      |> add_improvable_syntax
    47.1 --- a/src/Pure/Isar/proof_context.ML	Mon May 03 07:59:51 2010 +0200
    47.2 +++ b/src/Pure/Isar/proof_context.ML	Mon May 03 14:25:56 2010 +0200
    47.3 @@ -9,7 +9,7 @@
    47.4  signature PROOF_CONTEXT =
    47.5  sig
    47.6    val theory_of: Proof.context -> theory
    47.7 -  val init: theory -> Proof.context
    47.8 +  val init_global: theory -> Proof.context
    47.9    type mode
   47.10    val mode_default: mode
   47.11    val mode_stmt: mode
    48.1 --- a/src/Pure/Isar/proof_display.ML	Mon May 03 07:59:51 2010 +0200
    48.2 +++ b/src/Pure/Isar/proof_display.ML	Mon May 03 14:25:56 2010 +0200
    48.3 @@ -48,7 +48,7 @@
    48.4  
    48.5  fun pretty_theorems_diff verbose prev_thys thy =
    48.6    let
    48.7 -    val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
    48.8 +    val pretty_fact = ProofContext.pretty_fact (ProofContext.init_global thy);
    48.9      val facts = PureThy.facts_of thy;
   48.10      val thmss =
   48.11        Facts.dest_static (map PureThy.facts_of prev_thys) facts
    49.1 --- a/src/Pure/Isar/skip_proof.ML	Mon May 03 07:59:51 2010 +0200
    49.2 +++ b/src/Pure/Isar/skip_proof.ML	Mon May 03 14:25:56 2010 +0200
    49.3 @@ -39,6 +39,6 @@
    49.4        else tac args st);
    49.5  
    49.6  fun prove_global thy xs asms prop tac =
    49.7 -  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
    49.8 +  Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
    49.9  
   49.10  end;
    50.1 --- a/src/Pure/Isar/specification.ML	Mon May 03 07:59:51 2010 +0200
    50.2 +++ b/src/Pure/Isar/specification.ML	Mon May 03 14:25:56 2010 +0200
    50.3 @@ -169,7 +169,7 @@
    50.4  
    50.5  fun gen_axioms do_print prep raw_vars raw_specs thy =
    50.6    let
    50.7 -    val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
    50.8 +    val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init_global thy);
    50.9      val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
   50.10  
   50.11      (*consts*)
    51.1 --- a/src/Pure/Isar/theory_target.ML	Mon May 03 07:59:51 2010 +0200
    51.2 +++ b/src/Pure/Isar/theory_target.ML	Mon May 03 14:25:56 2010 +0200
    51.3 @@ -114,7 +114,7 @@
    51.4  fun import_export_proof ctxt (name, raw_th) =
    51.5    let
    51.6      val thy = ProofContext.theory_of ctxt;
    51.7 -    val thy_ctxt = ProofContext.init thy;
    51.8 +    val thy_ctxt = ProofContext.init_global thy;
    51.9      val certT = Thm.ctyp_of thy;
   51.10      val cert = Thm.cterm_of thy;
   51.11  
   51.12 @@ -213,7 +213,7 @@
   51.13  
   51.14  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   51.15    let
   51.16 -    val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   51.17 +    val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy);
   51.18      val target_ctxt = Local_Theory.target_of lthy;
   51.19  
   51.20      val (mx1, mx2, mx3) = fork_mixfix ta mx;
   51.21 @@ -286,7 +286,7 @@
   51.22  fun define ta ((b, mx), ((name, atts), rhs)) lthy =
   51.23    let
   51.24      val thy = ProofContext.theory_of lthy;
   51.25 -    val thy_ctxt = ProofContext.init thy;
   51.26 +    val thy_ctxt = ProofContext.init_global thy;
   51.27  
   51.28      val name' = Thm.def_binding_optional b name;
   51.29  
   51.30 @@ -342,7 +342,7 @@
   51.31  fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
   51.32    if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
   51.33    else if not (null overloading) then Overloading.init overloading
   51.34 -  else if not is_locale then ProofContext.init
   51.35 +  else if not is_locale then ProofContext.init_global
   51.36    else if not is_class then Locale.init target
   51.37    else Class_Target.init target;
   51.38  
   51.39 @@ -364,7 +364,7 @@
   51.40  
   51.41  fun gen_overloading prep_const raw_ops thy =
   51.42    let
   51.43 -    val ctxt = ProofContext.init thy;
   51.44 +    val ctxt = ProofContext.init_global thy;
   51.45      val ops = raw_ops |> map (fn (name, const, checked) =>
   51.46        (name, Term.dest_Const (prep_const ctxt const), checked));
   51.47    in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
    52.1 --- a/src/Pure/Proof/proof_syntax.ML	Mon May 03 07:59:51 2010 +0200
    52.2 +++ b/src/Pure/Proof/proof_syntax.ML	Mon May 03 14:25:56 2010 +0200
    52.3 @@ -206,7 +206,7 @@
    52.4        |> add_proof_syntax
    52.5        |> add_proof_atom_consts
    52.6          (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
    52.7 -      |> ProofContext.init
    52.8 +      |> ProofContext.init_global
    52.9        |> ProofContext.allow_dummies
   52.10        |> ProofContext.set_mode ProofContext.mode_schematic;
   52.11    in
    53.1 --- a/src/Pure/Syntax/syntax.ML	Mon May 03 07:59:51 2010 +0200
    53.2 +++ b/src/Pure/Syntax/syntax.ML	Mon May 03 14:25:56 2010 +0200
    53.3 @@ -850,10 +850,10 @@
    53.4  val read_term = singleton o read_terms;
    53.5  val read_prop = singleton o read_props;
    53.6  
    53.7 -val read_sort_global = read_sort o ProofContext.init;
    53.8 -val read_typ_global = read_typ o ProofContext.init;
    53.9 -val read_term_global = read_term o ProofContext.init;
   53.10 -val read_prop_global = read_prop o ProofContext.init;
   53.11 +val read_sort_global = read_sort o ProofContext.init_global;
   53.12 +val read_typ_global = read_typ o ProofContext.init_global;
   53.13 +val read_term_global = read_term o ProofContext.init_global;
   53.14 +val read_prop_global = read_prop o ProofContext.init_global;
   53.15  
   53.16  
   53.17  (* pretty = uncheck + unparse *)
   53.18 @@ -876,7 +876,7 @@
   53.19  structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
   53.20  val is_pretty_global = PrettyGlobal.get;
   53.21  val set_pretty_global = PrettyGlobal.put;
   53.22 -val init_pretty_global = set_pretty_global true o ProofContext.init;
   53.23 +val init_pretty_global = set_pretty_global true o ProofContext.init_global;
   53.24  
   53.25  val pretty_term_global = pretty_term o init_pretty_global;
   53.26  val pretty_typ_global = pretty_typ o init_pretty_global;
    54.1 --- a/src/Pure/axclass.ML	Mon May 03 07:59:51 2010 +0200
    54.2 +++ b/src/Pure/axclass.ML	Mon May 03 14:25:56 2010 +0200
    54.3 @@ -198,7 +198,7 @@
    54.4    (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
    54.5      SOME thm => Thm.transfer thy thm
    54.6    | NONE => error ("Unproven class relation " ^
    54.7 -      Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
    54.8 +      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));
    54.9  
   54.10  fun put_trancl_classrel ((c1, c2), th) thy =
   54.11    let
   54.12 @@ -245,7 +245,7 @@
   54.13    (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
   54.14      SOME (thm, _) => Thm.transfer thy thm
   54.15    | NONE => error ("Unproven type arity " ^
   54.16 -      Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
   54.17 +      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));
   54.18  
   54.19  fun thynames_of_arity thy (c, a) =
   54.20    Symtab.lookup_list (proven_arities_of thy) a
   54.21 @@ -357,7 +357,7 @@
   54.22    in (c1, c2) end;
   54.23  
   54.24  fun read_classrel thy raw_rel =
   54.25 -  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
   54.26 +  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init_global thy)) raw_rel)
   54.27      handle TYPE (msg, _, _) => error msg;
   54.28  
   54.29  
   54.30 @@ -461,7 +461,7 @@
   54.31  
   54.32  fun prove_classrel raw_rel tac thy =
   54.33    let
   54.34 -    val ctxt = ProofContext.init thy;
   54.35 +    val ctxt = ProofContext.init_global thy;
   54.36      val (c1, c2) = cert_classrel thy raw_rel;
   54.37      val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
   54.38        cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
   54.39 @@ -475,7 +475,7 @@
   54.40  
   54.41  fun prove_arity raw_arity tac thy =
   54.42    let
   54.43 -    val ctxt = ProofContext.init thy;
   54.44 +    val ctxt = ProofContext.init_global thy;
   54.45      val arity = ProofContext.cert_arity ctxt raw_arity;
   54.46      val names = map (prefix arity_prefix) (Logic.name_arities arity);
   54.47      val props = Logic.mk_arities arity;
   54.48 @@ -509,7 +509,7 @@
   54.49  
   54.50  fun define_class (bclass, raw_super) raw_params raw_specs thy =
   54.51    let
   54.52 -    val ctxt = ProofContext.init thy;
   54.53 +    val ctxt = ProofContext.init_global thy;
   54.54      val pp = Syntax.pp ctxt;
   54.55  
   54.56  
   54.57 @@ -623,7 +623,7 @@
   54.58      (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
   54.59  
   54.60  fun ax_arity prep =
   54.61 -  axiomatize (prep o ProofContext.init) Logic.mk_arities
   54.62 +  axiomatize (prep o ProofContext.init_global) Logic.mk_arities
   54.63      (map (prefix arity_prefix) o Logic.name_arities) add_arity;
   54.64  
   54.65  fun class_const c =
   54.66 @@ -643,7 +643,7 @@
   54.67  in
   54.68  
   54.69  val axiomatize_class = ax_class Sign.certify_class cert_classrel;
   54.70 -val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel;
   54.71 +val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init_global) read_classrel;
   54.72  val axiomatize_classrel = ax_classrel cert_classrel;
   54.73  val axiomatize_classrel_cmd = ax_classrel read_classrel;
   54.74  val axiomatize_arity = ax_arity ProofContext.cert_arity;
    55.1 --- a/src/Pure/codegen.ML	Mon May 03 07:59:51 2010 +0200
    55.2 +++ b/src/Pure/codegen.ML	Mon May 03 14:25:56 2010 +0200
    55.3 @@ -822,7 +822,7 @@
    55.4  
    55.5  val generate_code_i = gen_generate_code Sign.cert_term;
    55.6  val generate_code =
    55.7 -  gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init);
    55.8 +  gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init_global);
    55.9  
   55.10  
   55.11  (**** Reflection ****)
   55.12 @@ -908,7 +908,7 @@
   55.13  
   55.14  fun eval_term thy t =
   55.15    let
   55.16 -    val ctxt = ProofContext.init thy;
   55.17 +    val ctxt = ProofContext.init_global thy;
   55.18      val e =
   55.19        let
   55.20          val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    56.1 --- a/src/Pure/context.ML	Mon May 03 07:59:51 2010 +0200
    56.2 +++ b/src/Pure/context.ML	Mon May 03 14:25:56 2010 +0200
    56.3 @@ -20,7 +20,7 @@
    56.4    structure ProofContext:
    56.5    sig
    56.6      val theory_of: Proof.context -> theory
    56.7 -    val init: theory -> Proof.context
    56.8 +    val init_global: theory -> Proof.context
    56.9    end
   56.10  end;
   56.11  
   56.12 @@ -481,7 +481,7 @@
   56.13  structure ProofContext =
   56.14  struct
   56.15    val theory_of = theory_of_proof;
   56.16 -  fun init thy = Proof.Context (init_data thy, check_thy thy);
   56.17 +  fun init_global thy = Proof.Context (init_data thy, check_thy thy);
   56.18  end;
   56.19  
   56.20  structure Proof_Data =
   56.21 @@ -529,7 +529,7 @@
   56.22  fun proof_map f = the_proof o f o Proof;
   56.23  
   56.24  val theory_of = cases I ProofContext.theory_of;
   56.25 -val proof_of = cases ProofContext.init I;
   56.26 +val proof_of = cases ProofContext.init_global I;
   56.27  
   56.28  
   56.29  
    57.1 --- a/src/Pure/goal.ML	Mon May 03 07:59:51 2010 +0200
    57.2 +++ b/src/Pure/goal.ML	Mon May 03 14:25:56 2010 +0200
    57.3 @@ -211,7 +211,7 @@
    57.4  fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
    57.5  
    57.6  fun prove_global thy xs asms prop tac =
    57.7 -  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
    57.8 +  Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
    57.9  
   57.10  
   57.11  
    58.1 --- a/src/Pure/meta_simplifier.ML	Mon May 03 07:59:51 2010 +0200
    58.2 +++ b/src/Pure/meta_simplifier.ML	Mon May 03 14:25:56 2010 +0200
    58.3 @@ -299,7 +299,7 @@
    58.4  in
    58.5  
    58.6  fun print_term_global ss warn a thy t =
    58.7 -  print_term ss warn (K a) t (ProofContext.init thy);
    58.8 +  print_term ss warn (K a) t (ProofContext.init_global thy);
    58.9  
   58.10  fun if_enabled (Simpset ({context, ...}, _)) flag f =
   58.11    (case context of
   58.12 @@ -355,7 +355,7 @@
   58.13  fun context ctxt =
   58.14    map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
   58.15  
   58.16 -val global_context = context o ProofContext.init;
   58.17 +val global_context = context o ProofContext.init_global;
   58.18  
   58.19  fun activate_context thy ss =
   58.20    let
    59.1 --- a/src/Pure/old_goals.ML	Mon May 03 07:59:51 2010 +0200
    59.2 +++ b/src/Pure/old_goals.ML	Mon May 03 14:25:56 2010 +0200
    59.3 @@ -219,7 +219,7 @@
    59.4  
    59.5  fun simple_read_term thy T s =
    59.6    let
    59.7 -    val ctxt = ProofContext.init thy
    59.8 +    val ctxt = ProofContext.init_global thy
    59.9        |> ProofContext.allow_dummies
   59.10        |> ProofContext.set_mode ProofContext.mode_schematic;
   59.11      val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    60.1 --- a/src/Pure/sign.ML	Mon May 03 07:59:51 2010 +0200
    60.2 +++ b/src/Pure/sign.ML	Mon May 03 14:25:56 2010 +0200
    60.3 @@ -361,7 +361,7 @@
    60.4  
    60.5  fun gen_syntax change_gram parse_typ mode args thy =
    60.6    let
    60.7 -    val ctxt = ProofContext.init thy;
    60.8 +    val ctxt = ProofContext.init_global thy;
    60.9      fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
   60.10        handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
   60.11    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
   60.12 @@ -398,7 +398,7 @@
   60.13  
   60.14  fun gen_add_consts parse_typ raw_args thy =
   60.15    let
   60.16 -    val ctxt = ProofContext.init thy;
   60.17 +    val ctxt = ProofContext.init_global thy;
   60.18      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
   60.19      fun prep (b, raw_T, mx) =
   60.20        let
   60.21 @@ -497,7 +497,7 @@
   60.22  
   60.23  fun gen_trrules f args thy = thy |> map_syn (fn syn =>
   60.24    let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
   60.25 -  in f (ProofContext.init thy) (is_logtype thy) syn rules syn end);
   60.26 +  in f (ProofContext.init_global thy) (is_logtype thy) syn rules syn end);
   60.27  
   60.28  val add_trrules = gen_trrules Syntax.update_trrules;
   60.29  val del_trrules = gen_trrules Syntax.remove_trrules;
    61.1 --- a/src/Pure/simplifier.ML	Mon May 03 07:59:51 2010 +0200
    61.2 +++ b/src/Pure/simplifier.ML	Mon May 03 14:25:56 2010 +0200
    61.3 @@ -127,7 +127,7 @@
    61.4  fun map_simpset f = Context.theory_map (map_ss f);
    61.5  fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
    61.6  fun global_simpset_of thy =
    61.7 -  MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
    61.8 +  MetaSimplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy));
    61.9  
   61.10  fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
   61.11  fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
    62.1 --- a/src/Pure/theory.ML	Mon May 03 07:59:51 2010 +0200
    62.2 +++ b/src/Pure/theory.ML	Mon May 03 14:25:56 2010 +0200
    62.3 @@ -238,7 +238,7 @@
    62.4  
    62.5  fun check_def thy unchecked overloaded (b, tm) defs =
    62.6    let
    62.7 -    val ctxt = ProofContext.init thy;
    62.8 +    val ctxt = ProofContext.init_global thy;
    62.9      val name = Sign.full_name thy b;
   62.10      val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
   62.11        handle TERM (msg, _) => error msg;
    63.1 --- a/src/Pure/variable.ML	Mon May 03 07:59:51 2010 +0200
    63.2 +++ b/src/Pure/variable.ML	Mon May 03 14:25:56 2010 +0200
    63.3 @@ -235,7 +235,7 @@
    63.4  val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
    63.5  
    63.6  val declare_thm = Thm.fold_terms declare_internal;
    63.7 -fun global_thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
    63.8 +fun global_thm_context th = declare_thm th (ProofContext.init_global (Thm.theory_of_thm th));
    63.9  
   63.10  
   63.11  (* renaming term/type frees *)
    64.1 --- a/src/Tools/Code/code_eval.ML	Mon May 03 07:59:51 2010 +0200
    64.2 +++ b/src/Tools/Code/code_eval.ML	Mon May 03 14:25:56 2010 +0200
    64.3 @@ -47,7 +47,7 @@
    64.4  
    64.5  fun eval some_target reff postproc thy t args =
    64.6    let
    64.7 -    val ctxt = ProofContext.init thy;
    64.8 +    val ctxt = ProofContext.init_global thy;
    64.9      fun evaluator naming program ((_, (_, ty)), t) deps =
   64.10        let
   64.11          val _ = if Code_Thingol.contains_dictvar t then
    65.1 --- a/src/Tools/Code/code_preproc.ML	Mon May 03 07:59:51 2010 +0200
    65.2 +++ b/src/Tools/Code/code_preproc.ML	Mon May 03 14:25:56 2010 +0200
    65.3 @@ -87,7 +87,7 @@
    65.4  
    65.5  fun add_unfold_post raw_thm thy =
    65.6    let
    65.7 -    val thm = Local_Defs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
    65.8 +    val thm = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) raw_thm;
    65.9      val thm_sym = Thm.symmetric thm;
   65.10    in
   65.11      thy |> map_pre_post (fn (pre, post) =>
   65.12 @@ -157,7 +157,7 @@
   65.13  
   65.14  fun print_codeproc thy =
   65.15    let
   65.16 -    val ctxt = ProofContext.init thy;
   65.17 +    val ctxt = ProofContext.init_global thy;
   65.18      val pre = (#pre o the_thmproc) thy;
   65.19      val post = (#post o the_thmproc) thy;
   65.20      val functrans = (map fst o #functrans o the_thmproc) thy;
    66.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 03 07:59:51 2010 +0200
    66.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 03 14:25:56 2010 +0200
    66.3 @@ -210,7 +210,7 @@
    66.4  
    66.5      fun do_find () =
    66.6        let
    66.7 -        val ctxt = ProofContext.init (theory thy_name);
    66.8 +        val ctxt = ProofContext.init_global (theory thy_name);
    66.9          val query = get_query ();
   66.10          val (othmslen, thms) = apsnd rev
   66.11            (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
    67.1 --- a/src/Tools/nbe.ML	Mon May 03 07:59:51 2010 +0200
    67.2 +++ b/src/Tools/nbe.ML	Mon May 03 14:25:56 2010 +0200
    67.3 @@ -521,7 +521,7 @@
    67.4  
    67.5  fun compile_eval thy program vs_t deps =
    67.6    let
    67.7 -    val ctxt = ProofContext.init thy;
    67.8 +    val ctxt = ProofContext.init_global thy;
    67.9      val (gr, (_, idx_tab)) =
   67.10        Nbe_Functions.change thy (ensure_stmts ctxt program);
   67.11    in
    68.1 --- a/src/Tools/quickcheck.ML	Mon May 03 07:59:51 2010 +0200
    68.2 +++ b/src/Tools/quickcheck.ML	Mon May 03 14:25:56 2010 +0200
    68.3 @@ -295,7 +295,7 @@
    68.4  
    68.5  fun quickcheck_params_cmd args thy =
    68.6    let
    68.7 -    val ctxt = ProofContext.init thy;
    68.8 +    val ctxt = ProofContext.init_global thy;
    68.9      val f = fold (parse_test_param ctxt) args;
   68.10    in
   68.11      thy
    69.1 --- a/src/ZF/Tools/datatype_package.ML	Mon May 03 07:59:51 2010 +0200
    69.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon May 03 14:25:56 2010 +0200
    69.3 @@ -401,7 +401,7 @@
    69.4  
    69.5  fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
    69.6    let
    69.7 -    val ctxt = ProofContext.init thy;
    69.8 +    val ctxt = ProofContext.init_global thy;
    69.9      fun read_is strs =
   69.10        map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
   69.11        |> Syntax.check_terms ctxt;
    70.1 --- a/src/ZF/Tools/ind_cases.ML	Mon May 03 07:59:51 2010 +0200
    70.2 +++ b/src/ZF/Tools/ind_cases.ML	Mon May 03 14:25:56 2010 +0200
    70.3 @@ -46,7 +46,7 @@
    70.4  
    70.5  fun inductive_cases args thy =
    70.6    let
    70.7 -    val ctxt = ProofContext.init thy;
    70.8 +    val ctxt = ProofContext.init_global thy;
    70.9      val facts = args |> map (fn ((name, srcs), props) =>
   70.10        ((name, map (Attrib.attribute thy) srcs),
   70.11          map (Thm.no_attributes o single o smart_cases ctxt) props));
    71.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon May 03 07:59:51 2010 +0200
    71.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon May 03 14:25:56 2010 +0200
    71.3 @@ -163,7 +163,7 @@
    71.4  
    71.5  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
    71.6    let
    71.7 -    val ctxt = ProofContext.init thy;
    71.8 +    val ctxt = ProofContext.init_global thy;
    71.9      val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]);
   71.10      val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]);
   71.11      val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
    72.1 --- a/src/ZF/Tools/inductive_package.ML	Mon May 03 07:59:51 2010 +0200
    72.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon May 03 14:25:56 2010 +0200
    72.3 @@ -62,7 +62,7 @@
    72.4    raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
    72.5  let
    72.6    val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
    72.7 -  val ctxt = ProofContext.init thy;
    72.8 +  val ctxt = ProofContext.init_global thy;
    72.9  
   72.10    val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
   72.11    val (intr_names, intr_tms) = split_list (map fst intr_specs);
   72.12 @@ -174,7 +174,7 @@
   72.13      |> Sign.add_path big_rec_base_name
   72.14      |> PureThy.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
   72.15  
   72.16 -  val ctxt1 = ProofContext.init thy1;
   72.17 +  val ctxt1 = ProofContext.init_global thy1;
   72.18  
   72.19  
   72.20    (*fetch fp definitions from the theory*)
   72.21 @@ -261,7 +261,7 @@
   72.22        THEN (PRIMITIVE (fold_rule part_rec_defs));
   72.23  
   72.24    (*Elimination*)
   72.25 -  val elim = rule_by_tactic (ProofContext.init thy1) basic_elim_tac
   72.26 +  val elim = rule_by_tactic (ProofContext.init_global thy1) basic_elim_tac
   72.27                   (unfold RS Ind_Syntax.equals_CollectD)
   72.28  
   72.29    (*Applies freeness of the given constructors, which *must* be unfolded by
   72.30 @@ -554,7 +554,7 @@
   72.31  fun add_inductive (srec_tms, sdom_sum) intr_srcs
   72.32      (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   72.33    let
   72.34 -    val ctxt = ProofContext.init thy;
   72.35 +    val ctxt = ProofContext.init_global thy;
   72.36      val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
   72.37        #> Syntax.check_terms ctxt;
   72.38