renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
--- 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
--- 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
--- 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)
--- 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
--- 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);
--- 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 =
--- 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
--- 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";
--- 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
--- 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 []
--- 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;
--- 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;
--- 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 " "
--- 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 =
--- 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
--- 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
--- 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)
--- 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))
--- 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)
--- 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
--- 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))
--- 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)
--- 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*)
--- 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;
--- 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,
--- 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
--- 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;
--- 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
--- 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;
--- 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,
--- 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);
--- 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;
--- 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);
--- 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;
--- 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;
--- 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 *)
--- 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)
--- 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*)
--- 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;
--- 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) (
--- 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;
--- 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
--- 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;
--- 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;
--- 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;
--- 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
--- 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
--- 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
--- 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;
--- 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*)
--- 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;
--- 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
--- 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;
--- 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;
--- 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
--- 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;
--- 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);
--- 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
--- 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;
--- 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;
--- 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);
--- 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;
--- 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 *)
--- 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
--- 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;
--- 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);
--- 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
--- 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
--- 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;
--- 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));
--- 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;
--- 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;