# HG changeset patch # User wenzelm # Date 1272977070 -7200 # Node ID 30bd207ec222863d36e723f010680c76750f3bbd # Parent 4482c4a2cb727ffe16b02db3c68c9f38a4df86a6# Parent 2fd4e2c766366b47817634c23688358969fdf2c6 merged diff -r 4482c4a2cb72 -r 30bd207ec222 NEWS --- 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 *** diff -r 4482c4a2cb72 -r 30bd207ec222 doc-src/IsarImplementation/Thy/Prelim.thy --- 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} diff -r 4482c4a2cb72 -r 30bd207ec222 doc-src/IsarImplementation/Thy/document/Prelim.tex --- 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}% diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Boogie/Tools/boogie_commands.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Boogie/Tools/boogie_loader.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Import/proof_kernel.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Import/shuffler.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Matrix/cplex/matrixlp.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Mutabelle/Mutabelle.thy --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Mutabelle/mutabelle.ML --- 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); diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Mutabelle/mutabelle_extra.ML --- 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 = diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Nominal/nominal_datatype.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Nominal/nominal_fresh_fun.ML --- 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"; diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Statespace/state_space.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Datatype/datatype_codegen.ML --- 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 [] diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Datatype/datatype_data.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Function/size.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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 " " diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 = diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- 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) diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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)) diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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) diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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'] diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/TFL/post.ML --- 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) diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/TFL/rules.ML --- 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) diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/TFL/tfl.ML --- 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 () diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/choice_specification.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/cnf_funcs.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/inductive_codegen.ML --- 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, diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/inductive_realizer.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/old_primrec.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/recdef.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/record.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/typecopy.ML --- 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, diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOL/Tools/typedef.ML --- 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); diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOLCF/Tools/Domain/domain_theorems.ML --- 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); diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOLCF/Tools/pcpodef.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/HOLCF/Tools/repdef.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Provers/classical.ML --- 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 *) diff -r 4482c4a2cb72 -r 30bd207ec222 src/Provers/quantifier1.ML --- 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) diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/class.ML --- 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*) diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/class_target.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/code.ML --- 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) ( diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/constdefs.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/expression.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/local_theory.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/locale.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/object_logic.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/overloading.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/proof_context.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/proof_display.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/skip_proof.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/specification.ML --- 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*) diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Isar/theory_target.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Proof/extraction.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Proof/proof_syntax.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Proof/reconstruct.ML --- 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); diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/Syntax/syntax.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/axclass.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/codegen.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/context.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/drule.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/goal.ML --- 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); diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/meta_simplifier.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/old_goals.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/proofterm.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/sign.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/simplifier.ML --- 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); diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/term_subst.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/theory.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/thm.ML --- 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, diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/type.ML --- 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) diff -r 4482c4a2cb72 -r 30bd207ec222 src/Pure/variable.ML --- 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 = diff -r 4482c4a2cb72 -r 30bd207ec222 src/Tools/Code/code_eval.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Tools/Code/code_preproc.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/Tools/WWW_Find/find_theorems.ML --- 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); diff -r 4482c4a2cb72 -r 30bd207ec222 src/Tools/nbe.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/Tools/quickcheck.ML --- 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 diff -r 4482c4a2cb72 -r 30bd207ec222 src/ZF/Tools/datatype_package.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/ZF/Tools/ind_cases.ML --- 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)); diff -r 4482c4a2cb72 -r 30bd207ec222 src/ZF/Tools/induct_tacs.ML --- 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; diff -r 4482c4a2cb72 -r 30bd207ec222 src/ZF/Tools/inductive_package.ML --- 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;