--- a/NEWS Tue May 04 14:10:42 2010 +0200
+++ b/NEWS Tue May 04 14:44:30 2010 +0200
@@ -368,6 +368,12 @@
* Configuration options now admit dynamic default values, depending on
the context or even global references.
+* Most operations that refer to a global context are named
+accordingly, e.g. Simplifier.global_context or
+ProofContext.init_global. There are some situations where a global
+context actually works, but under normal circumstances one needs to
+pass the proper local context through the code!
+
*** System ***
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Tue May 04 14:10:42 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Tue May 04 14:44:30 2010 +0200
@@ -243,7 +243,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type Proof.context} \\
- @{index_ML ProofContext.init: "theory -> Proof.context"} \\
+ @{index_ML ProofContext.init_global: "theory -> Proof.context"} \\
@{index_ML ProofContext.theory_of: "Proof.context -> theory"} \\
@{index_ML ProofContext.transfer: "theory -> Proof.context -> Proof.context"} \\
\end{mldecls}
@@ -254,7 +254,7 @@
of this type are essentially pure values, with a sliding reference
to the background theory.
- \item @{ML ProofContext.init}~@{text "thy"} produces a proof context
+ \item @{ML ProofContext.init_global}~@{text "thy"} produces a proof context
derived from @{text "thy"}, initializing all data.
\item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the
@@ -305,7 +305,7 @@
\item @{ML Context.proof_of}~@{text "context"} always produces a
proof context from the generic @{text "context"}, using @{ML
- "ProofContext.init"} as required (note that this re-initializes the
+ "ProofContext.init_global"} as required (note that this re-initializes the
context data with each invocation).
\end{description}
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 04 14:10:42 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Tue May 04 14:44:30 2010 +0200
@@ -282,7 +282,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{Proof.context}\verb|type Proof.context| \\
- \indexdef{}{ML}{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
+ \indexdef{}{ML}{ProofContext.init\_global}\verb|ProofContext.init_global: theory -> Proof.context| \\
\indexdef{}{ML}{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
\indexdef{}{ML}{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
\end{mldecls}
@@ -293,7 +293,7 @@
of this type are essentially pure values, with a sliding reference
to the background theory.
- \item \verb|ProofContext.init|~\isa{thy} produces a proof context
+ \item \verb|ProofContext.init_global|~\isa{thy} produces a proof context
derived from \isa{thy}, initializing all data.
\item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
@@ -355,7 +355,7 @@
theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
\item \verb|Context.proof_of|~\isa{context} always produces a
- proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
+ proof context from the generic \isa{context}, using \verb|ProofContext.init_global| as required (note that this re-initializes the
context data with each invocation).
\end{description}%
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue May 04 14:44:30 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)
@@ -2065,7 +2065,7 @@
let
val (HOLThm args) = norm_hthm (theory_of_thm th) hth
in
- apsnd strip_shyps args
+ apsnd Thm.strip_shyps args
end
fun to_isa_term tm = tm
--- a/src/HOL/Import/shuffler.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Tue May 04 14:44:30 2010 +0200
@@ -502,7 +502,7 @@
t |> disamb_bound thy
|> chain (Simplifier.full_rewrite ss)
|> chain eta_conversion
- |> strip_shyps
+ |> Thm.strip_shyps
val _ = message ("norm_term: " ^ (string_of_thm th))
in
th
--- a/src/HOL/Matrix/cplex/matrixlp.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML Tue May 04 14:44:30 2010 +0200
@@ -81,7 +81,7 @@
fun matrix_simplify th =
let
val simp_th = matrix_compute (cprop_of th)
- val th = strip_shyps (equal_elim simp_th th)
+ val th = Thm.strip_shyps (equal_elim simp_th th)
fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
in
removeTrue th
--- a/src/HOL/Mutabelle/Mutabelle.thy Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Mutabelle/Mutabelle.thy Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Function/size.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Tue May 04 14:44:30 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/Quotient/quotient_tacs.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue May 04 14:44:30 2010 +0200
@@ -48,7 +48,7 @@
fun atomize_thm thm =
let
- val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
+ val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
val thm'' = Object_Logic.atomize (cprop_of thm')
in
@{thm equal_elim_rule1} OF [thm'', thm']
--- a/src/HOL/Tools/TFL/post.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML Tue May 04 14:44:30 2010 +0200
@@ -140,8 +140,8 @@
fun simplify_defn strict thy cs ss congs wfs id pats def0 =
let
- val ctxt = ProofContext.init thy
- val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
+ val ctxt = ProofContext.init_global thy
+ val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
val {rules,rows,TCs,full_pats_TCs} =
Prim.post_definition congs (thy, (def,pats))
val {lhs=f,rhs} = S.dest_eq (concl def)
--- a/src/HOL/Tools/TFL/rules.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue May 04 14:44:30 2010 +0200
@@ -134,9 +134,8 @@
in fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
end;
-(* freezeT expensive! *)
fun UNDISCH thm =
- let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
+ let val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm)))
in Thm.implies_elim (thm RS mp) (ASSUME tm) end
handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
| THM _ => raise RULES_ERR "UNDISCH" "";
@@ -252,7 +251,7 @@
| place _ _ = raise RULES_ERR "organize" "not a permutation.2"
in place
end;
-(* freezeT expensive! *)
+
fun DISJ_CASESL disjth thl =
let val c = cconcl disjth
fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
@@ -265,7 +264,7 @@
| DL th (th1::rst) =
let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
- in DL (Thm.freezeT disjth) (organize eq tml thl)
+ in DL disjth (organize eq tml thl)
end;
@@ -814,7 +813,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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Tue May 04 14:44:30 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*)
@@ -541,7 +541,7 @@
thy
|> PureThy.add_defs false
[Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
- val def = Thm.freezeT def0;
+ val def = Thm.unvarify_global def0;
val dummy =
if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
else ()
--- a/src/HOL/Tools/choice_specification.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Tue May 04 14:44:30 2010 +0200
@@ -78,10 +78,9 @@
| NONE => mk_definitional cos arg
end
-fun add_specification axiomatic cos arg =
- arg |> apsnd Thm.freezeT
- |> proc_exprop axiomatic cos
- |> apsnd Drule.export_without_context
+fun add_specification axiomatic cos =
+ proc_exprop axiomatic cos
+ #> apsnd Drule.export_without_context
(* Collect all intances of constants in term *)
@@ -217,15 +216,16 @@
then writeln "specification"
else ()
in
- arg |> apsnd Thm.freezeT
+ arg |> apsnd Thm.unvarify_global
|> process_all (zip3 alt_names rew_imps frees)
end
- fun after_qed [[thm]] = ProofContext.theory (fn thy =>
- #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
+ fun after_qed [[thm]] = (ProofContext.theory (fn thy =>
+ #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm)))));
in
thy
- |> ProofContext.init
+ |> ProofContext.init_global
+ |> Variable.declare_term ex_prop
|> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
end;
--- a/src/HOL/Tools/cnf_funcs.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Tue May 04 14:44:30 2010 +0200
@@ -436,8 +436,8 @@
val var = new_free ()
val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *)
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
- val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
- val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
@@ -447,8 +447,8 @@
val var = new_free ()
val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *)
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
- val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
- val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
in
iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *)
end
@@ -467,8 +467,8 @@
val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *)
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *)
- val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
- val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
in
iff_trans OF [thm1, thm5]
end
--- a/src/HOL/Tools/inductive_codegen.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/old_primrec.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/recdef.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/record.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOL/Tools/typedef.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Provers/classical.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Provers/quantifier1.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/class.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/class_target.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/code.ML Tue May 04 14:44:30 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);
@@ -778,7 +778,7 @@
val _ = if c = const_abs_eqn thy abs_thm then ()
else error ("Wrong head of abstract code equation,\nexpected constant "
^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
- in Abstract (Thm.freezeT abs_thm, tyco) end;
+ in Abstract (Thm.legacy_freezeT abs_thm, tyco) end;
fun constrain_cert thy sorts (Equations (cert_thm, propers)) =
let
@@ -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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/constdefs.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/expression.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/locale.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/object_logic.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/overloading.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/proof_display.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/skip_proof.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/specification.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML Tue May 04 14:44:30 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/extraction.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Tue May 04 14:44:30 2010 +0200
@@ -136,8 +136,7 @@
| strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
| strip_abs _ _ = error "strip_abs: not an abstraction";
-fun prf_subst_TVars tye =
- map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
+val prf_subst_TVars = map_proof_types o typ_subst_TVars;
fun relevant_vars types prop = List.foldr (fn
(Var ((a, _), T), vs) => (case strip_type T of
--- a/src/Pure/Proof/proof_syntax.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue May 04 14:44:30 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/Proof/reconstruct.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue May 04 14:44:30 2010 +0200
@@ -376,8 +376,7 @@
val varify = map_type_tfree (fn p as (a, S) =>
if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
in
- (maxidx', prfs', map_proof_terms (subst_TVars tye o
- map_types varify) (typ_subst_TVars tye o varify) prf)
+ (maxidx', prfs', map_proof_types (typ_subst_TVars tye o varify) prf)
end
| expand maxidx prfs prf = (maxidx, prfs, prf);
--- a/src/Pure/Syntax/syntax.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/axclass.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/codegen.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/context.ML Tue May 04 14:44:30 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/drule.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/drule.ML Tue May 04 14:44:30 2010 +0200
@@ -307,7 +307,7 @@
Similar code in type/freeze_thaw*)
fun legacy_freeze_thaw_robust th =
- let val fth = Thm.freezeT th
+ let val fth = Thm.legacy_freezeT th
val thy = Thm.theory_of_thm fth
val {prop, tpairs, ...} = rep_thm fth
in
@@ -329,7 +329,7 @@
(*Basic version of the function above. No option to rename Vars apart in thaw.
The Frees created from Vars have nice names.*)
fun legacy_freeze_thaw th =
- let val fth = Thm.freezeT th
+ let val fth = Thm.legacy_freezeT th
val thy = Thm.theory_of_thm fth
val {prop, tpairs, ...} = rep_thm fth
in
--- a/src/Pure/goal.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/goal.ML Tue May 04 14:44:30 2010 +0200
@@ -137,7 +137,8 @@
Thm.adjust_maxidx_thm ~1 #>
Drule.implies_intr_list assms #>
Drule.forall_intr_list fixes #>
- Thm.generalize (map #1 tfrees, []) 0);
+ Thm.generalize (map #1 tfrees, []) 0 #>
+ Thm.strip_shyps);
val local_result =
Thm.future global_result global_prop
|> Thm.instantiate (instT, [])
@@ -211,7 +212,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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/meta_simplifier.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/old_goals.ML Tue May 04 14:44:30 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/proofterm.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/proofterm.ML Tue May 04 14:44:30 2010 +0200
@@ -58,8 +58,10 @@
val strip_combt: proof -> proof * term option list
val strip_combP: proof -> proof * proof list
val strip_thm: proof_body -> proof_body
- val map_proof_terms_option: (term -> term option) -> (typ -> typ option) -> proof -> proof
+ val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
+ val map_proof_types_same: typ Same.operation -> proof Same.operation
val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
+ val map_proof_types: (typ -> typ) -> proof -> proof
val fold_proof_terms: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
val maxidx_proof: proof -> int -> int
val size_of_proof: proof -> int
@@ -80,7 +82,7 @@
val implies_intr_proof: term -> proof -> proof
val forall_intr_proof: term -> string -> proof -> proof
val varify_proof: term -> (string * sort) list -> proof -> proof
- val freezeT: term -> proof -> proof
+ val legacy_freezeT: term -> proof -> proof
val rotate_proof: term list -> term -> int -> proof -> proof
val permute_prems_prf: term list -> int -> int -> proof -> proof
val generalize: string list * string list -> int -> proof -> proof
@@ -106,6 +108,8 @@
val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof
val equal_intr: term -> term -> proof -> proof -> proof
val equal_elim: term -> term -> proof -> proof -> proof
+ val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
+ sort list -> proof -> proof
val axm_proof: string -> term -> proof
val oracle_proof: string -> term -> oracle * proof
val promise_proof: theory -> serial -> term -> proof
@@ -273,10 +277,8 @@
val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
-fun map_proof_terms_option f g =
+fun map_proof_same term typ ofclass =
let
- val term = Same.function f;
- val typ = Same.function g;
val typs = Same.map typ;
fun proof (Abst (s, T, prf)) =
@@ -292,22 +294,23 @@
(proof prf1 %% Same.commit proof prf2
handle Same.SAME => prf1 %% proof prf2)
| proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
- | proof (OfClass (T, c)) = OfClass (typ T, c)
+ | proof (OfClass T_c) = ofclass T_c
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
| proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
| proof (PThm (i, ((a, prop, SOME Ts), body))) =
PThm (i, ((a, prop, SOME (typs Ts)), body))
| proof _ = raise Same.SAME;
- in Same.commit proof end;
+ in proof end;
+
+fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c));
+fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
fun same eq f x =
let val x' = f x
in if eq (x, x') then raise Same.SAME else x' end;
-fun map_proof_terms f g =
- map_proof_terms_option
- (fn t => SOME (same (op =) f t) handle Same.SAME => NONE)
- (fn T => SOME (same (op =) g T) handle Same.SAME => NONE);
+fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g));
+fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f));
fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
| fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
@@ -652,7 +655,7 @@
in
-fun freezeT t prf =
+fun legacy_freezeT t prf =
let
val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
@@ -696,17 +699,17 @@
(***** generalization *****)
fun generalize (tfrees, frees) idx =
- map_proof_terms_option
- (Term_Subst.generalize_option (tfrees, frees) idx)
- (Term_Subst.generalizeT_option tfrees idx);
+ Same.commit (map_proof_terms_same
+ (Term_Subst.generalize_same (tfrees, frees) idx)
+ (Term_Subst.generalizeT_same tfrees idx));
(***** instantiation *****)
fun instantiate (instT, inst) =
- map_proof_terms_option
- (Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst))
- (Term_Subst.instantiateT_option instT);
+ Same.commit (map_proof_terms_same
+ (Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst))
+ (Term_Subst.instantiateT_same instT));
(***** lifting *****)
@@ -757,9 +760,8 @@
end;
fun incr_indexes i =
- map_proof_terms_option
- (Same.capture (Logic.incr_indexes_same ([], i)))
- (Same.capture (Logic.incr_tvar_same i));
+ Same.commit (map_proof_terms_same
+ (Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i));
(***** proof by assumption *****)
@@ -884,6 +886,22 @@
equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
+(**** sort hypotheses ****)
+
+fun strip_shyps_proof algebra present witnessed extra_sorts prf =
+ let
+ fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
+ val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts;
+ val replacements = present @ extra @ witnessed;
+ fun replace T =
+ if exists (fn (T', _) => T' = T) present then raise Same.SAME
+ else
+ (case get_first (get (Type.sort_of_atyp T)) replacements of
+ SOME T' => T'
+ | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term");
+ in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
+
+
(***** axioms and theorems *****)
val proofs = Unsynchronized.ref 2;
--- a/src/Pure/sign.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/sign.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/simplifier.ML Tue May 04 14:44:30 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/term_subst.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/term_subst.ML Tue May 04 14:44:30 2010 +0200
@@ -13,6 +13,8 @@
val map_atyps_option: (typ -> typ option) -> term -> term option
val map_types_option: (typ -> typ option) -> term -> term option
val map_aterms_option: (term -> term option) -> term -> term option
+ val generalizeT_same: string list -> int -> typ Same.operation
+ val generalize_same: string list * string list -> int -> term Same.operation
val generalize: string list * string list -> int -> term -> term
val generalizeT: string list -> int -> typ -> typ
val generalize_option: string list * string list -> int -> term -> term option
@@ -21,12 +23,12 @@
val instantiate_maxidx:
((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
term -> int -> term * int
+ val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
term -> term
- val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
- val instantiate_option: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
- term -> term option
- val instantiateT_option: ((indexname * sort) * typ) list -> typ -> typ option
+ val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
+ val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
+ term Same.operation
val zero_var_indexes: term -> term
val zero_var_indexes_inst: term list ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list
@@ -70,8 +72,6 @@
(* generalization of fixed variables *)
-local
-
fun generalizeT_same [] _ _ = raise Same.SAME
| generalizeT_same tfrees idx ty =
let
@@ -99,16 +99,12 @@
| gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u);
in gen tm end;
-in
-
-fun generalize names i tm = generalize_same names i tm handle Same.SAME => tm;
-fun generalizeT names i ty = generalizeT_same names i ty handle Same.SAME => ty;
+fun generalize names i tm = Same.commit (generalize_same names i) tm;
+fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty;
fun generalize_option names i tm = SOME (generalize_same names i tm) handle Same.SAME => NONE;
fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle Same.SAME => NONE;
-end;
-
(* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
@@ -118,7 +114,7 @@
fun no_indexes1 inst = map no_index inst;
fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
-fun instantiateT_same maxidx instT ty =
+fun instT_same maxidx instT ty =
let
fun maxify i = if i > ! maxidx then maxidx := i else ();
@@ -134,11 +130,11 @@
| subst_typs [] = raise Same.SAME;
in subst_typ ty end;
-fun instantiate_same maxidx (instT, inst) tm =
+fun inst_same maxidx (instT, inst) tm =
let
fun maxify i = if i > ! maxidx then maxidx := i else ();
- val substT = instantiateT_same maxidx instT;
+ val substT = instT_same maxidx instT;
fun subst (Const (c, T)) = Const (c, substT T)
| subst (Free (x, T)) = Free (x, substT T)
| subst (Var ((x, i), T)) =
@@ -158,31 +154,23 @@
fun instantiateT_maxidx instT ty i =
let val maxidx = Unsynchronized.ref i
- in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
+ in (Same.commit (instT_same maxidx instT) ty, ! maxidx) end;
fun instantiate_maxidx insts tm i =
let val maxidx = Unsynchronized.ref i
- in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
+ in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
fun instantiateT [] ty = ty
- | instantiateT instT ty =
- (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
- handle Same.SAME => ty);
+ | instantiateT instT ty = Same.commit (instT_same (Unsynchronized.ref ~1) (no_indexes1 instT)) ty;
fun instantiate ([], []) tm = tm
- | instantiate insts tm =
- (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
- handle Same.SAME => tm);
+ | instantiate insts tm = Same.commit (inst_same (Unsynchronized.ref ~1) (no_indexes2 insts)) tm;
-fun instantiateT_option [] _ = NONE
- | instantiateT_option instT ty =
- (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
- handle Same.SAME => NONE);
+fun instantiateT_same [] _ = raise Same.SAME
+ | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty;
-fun instantiate_option ([], []) _ = NONE
- | instantiate_option insts tm =
- (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
- handle Same.SAME => NONE);
+fun instantiate_same ([], []) _ = raise Same.SAME
+ | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm;
end;
--- a/src/Pure/theory.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/theory.ML Tue May 04 14:44:30 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/thm.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/thm.ML Tue May 04 14:44:30 2010 +0200
@@ -69,7 +69,6 @@
val weaken: cterm -> thm -> thm
val weaken_sorts: sort list -> cterm -> cterm
val extra_shyps: thm -> sort list
- val strip_shyps: thm -> thm
(*meta rules*)
val assume: cterm -> thm
@@ -138,9 +137,10 @@
val varifyT_global: thm -> thm
val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val of_class: ctyp * class -> thm
+ val strip_shyps: thm -> thm
val unconstrainT: ctyp -> thm -> thm
val unconstrain_allTs: thm -> thm
- val freezeT: thm -> thm
+ val legacy_freezeT: thm -> thm
val assumption: int -> thm -> thm Seq.seq
val eq_assumption: int -> thm -> thm
val rotate_rule: int -> int -> thm -> thm
@@ -476,26 +476,6 @@
val sorts' = Sorts.union sorts more_sorts;
in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
-
-
-(** sort contexts of theorems **)
-
-(*remove extra sorts that are witnessed by type signature information*)
-fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
- | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
- let
- val thy = Theory.deref thy_ref;
- val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
- val extra = fold (Sorts.remove_sort o #2) present shyps;
- val witnessed = Sign.witness_sorts thy present extra;
- val extra' = fold (Sorts.remove_sort o #2) witnessed extra
- |> Sorts.minimal_sorts (Sign.classes_of thy);
- val shyps' = fold (Sorts.insert_sort o #2) present extra';
- in
- Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
- shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
- end;
-
(*dangling sort constraints of a thm*)
fun extra_shyps (th as Thm (_, {shyps, ...})) =
Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
@@ -532,6 +512,9 @@
fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
+fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
+ make_deriv promises oracles thms (f proof);
+
(* fulfilled proofs *)
@@ -565,14 +548,13 @@
(* future rule *)
-fun future_result i orig_thy orig_shyps orig_prop raw_thm =
+fun future_result i orig_thy orig_shyps orig_prop thm =
let
+ fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
+ val Thm (Deriv {promises, ...}, {thy_ref, shyps, hyps, tpairs, prop, ...}) = thm;
+
+ val _ = Theory.eq_thy (Theory.deref thy_ref, orig_thy) orelse err "bad theory";
val _ = Theory.check_thy orig_thy;
- val thm = strip_shyps (transfer orig_thy raw_thm);
- val _ = Theory.check_thy orig_thy;
- fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
-
- val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
val _ = prop aconv orig_prop orelse err "bad prop";
val _ = null tpairs orelse err "bad tpairs";
val _ = null hyps orelse err "bad hyps";
@@ -1220,6 +1202,25 @@
else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
end;
+(*Remove extra sorts that are witnessed by type signature information*)
+fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
+ | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
+ let
+ val thy = Theory.deref thy_ref;
+ val algebra = Sign.classes_of thy;
+
+ val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
+ val extra = fold (Sorts.remove_sort o #2) present shyps;
+ val witnessed = Sign.witness_sorts thy present extra;
+ val extra' = fold (Sorts.remove_sort o #2) witnessed extra
+ |> Sorts.minimal_sorts algebra;
+ val shyps' = fold (Sorts.insert_sort o #2) present extra';
+ in
+ Thm (deriv_rule_unconditional (Pt.strip_shyps_proof algebra present witnessed extra') der,
+ {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
+ shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
+ end;
+
(*Internalize sort constraints of type variable*)
fun unconstrainT
(Ctyp {thy_ref = thy_ref1, T, ...})
@@ -1266,14 +1267,14 @@
val varifyT_global = #2 o varifyT_global' [];
-(* Replace all TVars by new TFrees *)
-fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
+(* Replace all TVars by TFrees that are often new *)
+fun legacy_freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
let
val prop1 = attach_tpairs tpairs prop;
val prop2 = Type.legacy_freeze prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
in
- Thm (deriv_rule1 (Pt.freezeT prop1) der,
+ Thm (deriv_rule1 (Pt.legacy_freezeT prop1) der,
{thy_ref = thy_ref,
tags = [],
maxidx = maxidx_of_term prop2,
--- a/src/Pure/type.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/type.ML Tue May 04 14:44:30 2010 +0200
@@ -53,6 +53,7 @@
val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
(*special treatment of type vars*)
+ val sort_of_atyp: typ -> sort
val strip_sorts: typ -> typ
val no_tvars: typ -> typ
val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
@@ -271,6 +272,13 @@
(** special treatment of type vars **)
+(* sort_of_atyp *)
+
+fun sort_of_atyp (TFree (_, S)) = S
+ | sort_of_atyp (TVar (_, S)) = S
+ | sort_of_atyp T = raise TYPE ("sort_of_atyp", [T], []);
+
+
(* strip_sorts *)
fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts)
--- a/src/Pure/variable.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Pure/variable.ML Tue May 04 14:44:30 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 *)
@@ -376,9 +376,9 @@
val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
val tfrees = mk_tfrees [];
val idx = Proofterm.maxidx_proof prf ~1 + 1;
- val gen_term = Term_Subst.generalize_option (tfrees, frees) idx;
- val gen_typ = Term_Subst.generalizeT_option tfrees idx;
- in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
+ val gen_term = Term_Subst.generalize_same (tfrees, frees) idx;
+ val gen_typ = Term_Subst.generalizeT_same tfrees idx;
+ in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end;
fun gen_export (mk_tfrees, frees) ths =
--- a/src/Tools/Code/code_eval.ML Tue May 04 14:10:42 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Tools/nbe.ML Tue May 04 14:44:30 2010 +0200
@@ -105,14 +105,14 @@
|> Drule.cterm_rule Thm.varifyT_global
|> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) =>
(((v, 0), sort), TFree (v, sort'))) vs, []))
- |> Drule.cterm_rule Thm.freezeT
+ |> Drule.cterm_rule Thm.legacy_freezeT
|> conv
|> Thm.varifyT_global
|> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
|> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
(((v, 0), []), TVar ((v, 0), sort))) vs, [])
|> strip_of_class
- |> Thm.freezeT
+ |> Thm.legacy_freezeT
end;
fun lift_triv_classes_rew thy rew t =
@@ -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 Tue May 04 14:10:42 2010 +0200
+++ b/src/Tools/quickcheck.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Tue May 04 14:44:30 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 Tue May 04 14:10:42 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue May 04 14:44:30 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;