# HG changeset patch # User wenzelm # Date 1302963337 -7200 # Node ID 23f35299094493b974515d57b0d713e2474b3cac # Parent da8817d01e7c3c65902135e202493bb0bce7a592 modernized structure Proof_Context; diff -r da8817d01e7c -r 23f352990944 doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Sat Apr 16 16:15:37 2011 +0200 @@ -279,9 +279,9 @@ text %mlref {* \begin{mldecls} @{index_ML_type 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"} \\ + @{index_ML Proof_Context.init_global: "theory -> Proof.context"} \\ + @{index_ML Proof_Context.theory_of: "Proof.context -> theory"} \\ + @{index_ML Proof_Context.transfer: "theory -> Proof.context -> Proof.context"} \\ \end{mldecls} \begin{description} @@ -290,14 +290,14 @@ Elements of this type are essentially pure values, with a sliding reference to the background theory. - \item @{ML ProofContext.init_global}~@{text "thy"} produces a proof context + \item @{ML Proof_Context.init_global}~@{text "thy"} produces a proof context derived from @{text "thy"}, initializing all data. - \item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the + \item @{ML Proof_Context.theory_of}~@{text "ctxt"} selects the background theory from @{text "ctxt"}, dereferencing its internal @{ML_type theory_ref}. - \item @{ML ProofContext.transfer}~@{text "thy ctxt"} promotes the + \item @{ML Proof_Context.transfer}~@{text "thy ctxt"} promotes the background theory of @{text "ctxt"} to the super theory @{text "thy"}. @@ -354,11 +354,11 @@ \item @{ML Context.theory_of}~@{text "context"} always produces a theory from the generic @{text "context"}, using @{ML - "ProofContext.theory_of"} as required. + "Proof_Context.theory_of"} as required. \item @{ML Context.proof_of}~@{text "context"} always produces a proof context from the generic @{text "context"}, using @{ML - "ProofContext.init_global"} as required (note that this re-initializes the + "Proof_Context.init_global"} as required (note that this re-initializes the context data with each invocation). \end{description} diff -r da8817d01e7c -r 23f352990944 doc-src/IsarImplementation/Thy/Proof.thy --- a/doc-src/IsarImplementation/Thy/Proof.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Sat Apr 16 16:15:37 2011 +0200 @@ -314,7 +314,7 @@ exports result @{text "thm"} from the the @{text "inner"} context back into the @{text "outer"} one; @{text "is_goal = true"} means this is a goal context. The result is in HHF normal form. Note - that @{ML "ProofContext.export"} combines @{ML "Variable.export"} + that @{ML "Proof_Context.export"} combines @{ML "Variable.export"} and @{ML "Assumption.export"} in the canonical way. \end{description} @@ -341,7 +341,7 @@ text {* Note that the variables of the resulting rule are not generalized. This would have required to fix them properly in the context beforehand, and export wrt.\ variables afterwards (cf.\ @{ML - Variable.export} or the combined @{ML "ProofContext.export"}). *} + Variable.export} or the combined @{ML "Proof_Context.export"}). *} section {* Structured goals and results \label{sec:struct-goals} *} @@ -481,10 +481,10 @@ |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}]; *} ML_prf %"ML" {* - singleton (ProofContext.export ctxt1 ctxt0) @{thm refl}; + singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl}; *} ML_prf %"ML" {* - ProofContext.export ctxt1 ctxt0 [Thm.reflexive x] + Proof_Context.export ctxt1 ctxt0 [Thm.reflexive x] handle ERROR msg => (warning msg; []); *} end diff -r da8817d01e7c -r 23f352990944 doc-src/IsarImplementation/Thy/document/Prelim.tex --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Sat Apr 16 15:47:52 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Sat Apr 16 16:15:37 2011 +0200 @@ -331,9 +331,9 @@ \begin{isamarkuptext}% \begin{mldecls} \indexdef{}{ML type}{Proof.context}\verb|type 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| \\ + \indexdef{}{ML}{Proof\_Context.init\_global}\verb|Proof_Context.init_global: theory -> Proof.context| \\ + \indexdef{}{ML}{Proof\_Context.theory\_of}\verb|Proof_Context.theory_of: Proof.context -> theory| \\ + \indexdef{}{ML}{Proof\_Context.transfer}\verb|Proof_Context.transfer: theory -> Proof.context -> Proof.context| \\ \end{mldecls} \begin{description} @@ -342,14 +342,14 @@ Elements of this type are essentially pure values, with a sliding reference to the background theory. - \item \verb|ProofContext.init_global|~\isa{thy} produces a proof context + \item \verb|Proof_Context.init_global|~\isa{thy} produces a proof context derived from \isa{thy}, initializing all data. - \item \verb|ProofContext.theory_of|~\isa{ctxt} selects the + \item \verb|Proof_Context.theory_of|~\isa{ctxt} selects the background theory from \isa{ctxt}, dereferencing its internal \verb|theory_ref|. - \item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the + \item \verb|Proof_Context.transfer|~\isa{thy\ ctxt} promotes the background theory of \isa{ctxt} to the super theory \isa{thy}. \end{description}% @@ -432,10 +432,10 @@ constructors \verb|Context.Theory| and \verb|Context.Proof|. \item \verb|Context.theory_of|~\isa{context} always produces a - theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required. + theory from the generic \isa{context}, using \verb|Proof_Context.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_global| as required (note that this re-initializes the + proof context from the generic \isa{context}, using \verb|Proof_Context.init_global| as required (note that this re-initializes the context data with each invocation). \end{description}% diff -r da8817d01e7c -r 23f352990944 doc-src/IsarImplementation/Thy/document/Proof.tex --- a/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Apr 16 15:47:52 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Apr 16 16:15:37 2011 +0200 @@ -462,7 +462,7 @@ exports result \isa{thm} from the the \isa{inner} context back into the \isa{outer} one; \isa{is{\isaliteral{5F}{\isacharunderscore}}goal\ {\isaliteral{3D}{\isacharequal}}\ true} means this is a goal context. The result is in HHF normal form. Note - that \verb|ProofContext.export| combines \verb|Variable.export| + that \verb|Proof_Context.export| combines \verb|Variable.export| and \verb|Assumption.export| in the canonical way. \end{description}% @@ -532,7 +532,7 @@ \begin{isamarkuptext}% Note that the variables of the resulting rule are not generalized. This would have required to fix them properly in the - context beforehand, and export wrt.\ variables afterwards (cf.\ \verb|Variable.export| or the combined \verb|ProofContext.export|).% + context beforehand, and export wrt.\ variables afterwards (cf.\ \verb|Variable.export| or the combined \verb|Proof_Context.export|).% \end{isamarkuptext}% \isamarkuptrue% % @@ -786,7 +786,7 @@ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline \ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse% \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline -\ \ \ \ singleton\ {\isaliteral{28}{\isacharparenleft}}ProofContext{\isaliteral{2E}{\isachardot}}export\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ % +\ \ \ \ singleton\ {\isaliteral{28}{\isacharparenleft}}Proof{\isaliteral{5F}{\isacharunderscore}}Context{\isaliteral{2E}{\isachardot}}export\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ % \isaantiq thm\ refl{}% \endisaantiq @@ -794,7 +794,7 @@ \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline \ \ \isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}\isamarkupfalse% \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline -\ \ \ \ ProofContext{\isaliteral{2E}{\isachardot}}export\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}\ {\isaliteral{5B}{\isacharbrackleft}}Thm{\isaliteral{2E}{\isachardot}}reflexive\ x{\isaliteral{5D}{\isacharbrackright}}\isanewline +\ \ \ \ Proof{\isaliteral{5F}{\isacharunderscore}}Context{\isaliteral{2E}{\isachardot}}export\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}\ {\isaliteral{5B}{\isacharbrackleft}}Thm{\isaliteral{2E}{\isachardot}}reflexive\ x{\isaliteral{5D}{\isacharbrackright}}\isanewline \ \ \ \ \ \ handle\ ERROR\ msg\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}warning\ msg{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline \ \ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline \isacommand{end}\isamarkupfalse% diff -r da8817d01e7c -r 23f352990944 doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/doc-src/Main/Docs/Main_Doc.thy Sat Apr 16 16:15:37 2011 +0200 @@ -5,7 +5,7 @@ ML {* fun pretty_term_type_only ctxt (t, T) = - (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then () + (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then () else error "term_type_only: type mismatch"; Syntax.pretty_typ ctxt T) diff -r da8817d01e7c -r 23f352990944 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/doc-src/antiquote_setup.ML Sat Apr 16 16:15:37 2011 +0200 @@ -132,7 +132,7 @@ fun no_check _ _ = true; fun thy_check intern defined ctxt = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt in defined thy o intern thy end; fun check_tool name = diff -r da8817d01e7c -r 23f352990944 doc-src/more_antiquote.ML --- a/doc-src/more_antiquote.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/doc-src/more_antiquote.ML Sat Apr 16 16:15:37 2011 +0200 @@ -27,7 +27,7 @@ fun pretty_code_thm src ctxt raw_const = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val const = Code.check_const thy raw_const; val (_, eqngr) = Code_Preproc.obtain true thy [const] []; fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; diff -r da8817d01e7c -r 23f352990944 doc-src/rail.ML --- a/doc-src/rail.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/doc-src/rail.ML Sat Apr 16 16:15:37 2011 +0200 @@ -47,7 +47,7 @@ fun false_check _ _ = false; fun thy_check intern defined ctxt = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt in defined thy o intern thy end; fun check_tool name = diff -r da8817d01e7c -r 23f352990944 src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Sat Apr 16 16:15:37 2011 +0200 @@ -63,7 +63,7 @@ val (us, u) = split_goal t val assms = [((@{binding vc_trace}, []), map (rpair []) us)] in - pair [u] o snd o ProofContext.add_assms_i Assumption.assume_export assms + pair [u] o snd o Proof_Context.add_assms_i Assumption.assume_export assms end fun single_prove goal ctxt thm = @@ -100,16 +100,16 @@ | _ => (pair ts, K I)) val discharge = fold (Boogie_VCs.discharge o pair vc_name) - fun after_qed [thms] = ProofContext.background_theory (discharge (vcs ~~ thms)) + fun after_qed [thms] = Proof_Context.background_theory (discharge (vcs ~~ thms)) | after_qed _ = I in - ProofContext.init_global thy + Proof_Context.init_global thy |> fold Variable.auto_fixes ts |> (fn ctxt1 => ctxt1 |> prepare |-> (fn us => fn ctxt2 => ctxt2 |> Proof.theorem NONE (fn thmss => fn ctxt => - let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2 + let val export = map (finish ctxt1) o Proof_Context.export ctxt ctxt2 in after_qed (map export thmss) ctxt end) [map (rpair []) us])) end end @@ -196,7 +196,7 @@ end fun prove thy meth vc = - ProofContext.init_global thy + Proof_Context.init_global thy |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]] |> Proof.apply meth |> Seq.hd diff -r da8817d01e7c -r 23f352990944 src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Sat Apr 16 16:15:37 2011 +0200 @@ -234,7 +234,7 @@ in apsnd sort_fst_str (fold split axs ([], [])) end fun mark_axioms thy axs = - Boogie_Axioms.get (ProofContext.init_global thy) + Boogie_Axioms.get (Proof_Context.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 da8817d01e7c -r 23f352990944 src/HOL/Boogie/Tools/boogie_tactics.ML --- a/src/HOL/Boogie/Tools/boogie_tactics.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Sat Apr 16 16:15:37 2011 +0200 @@ -90,7 +90,7 @@ Seq.maps (fn (names, st) => CASES (Rule_Cases.make_common - (ProofContext.theory_of ctxt, + (Proof_Context.theory_of ctxt, Thm.prop_of (Rule_Cases.internalize_params st)) names) Tactical.all_tac st)) in diff -r da8817d01e7c -r 23f352990944 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Sat Apr 16 16:15:37 2011 +0200 @@ -3341,10 +3341,10 @@ end fun approximation_conv ctxt ct = - approximation_oracle (ProofContext.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt)); + approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt)); fun approximate ctxt t = - approximation_oracle (ProofContext.theory_of ctxt, t) + approximation_oracle (Proof_Context.theory_of ctxt, t) |> Thm.prop_of |> Logic.dest_equals |> snd; (* Should be in HOL.thy ? *) @@ -3366,16 +3366,16 @@ |> HOLogic.dest_list val p = prec |> HOLogic.mk_number @{typ nat} - |> Thm.cterm_of (ProofContext.theory_of ctxt) + |> Thm.cterm_of (Proof_Context.theory_of ctxt) in case taylor of NONE => let val n = vs |> length |> HOLogic.mk_number @{typ nat} - |> Thm.cterm_of (ProofContext.theory_of ctxt) + |> Thm.cterm_of (Proof_Context.theory_of ctxt) val s = vs |> map lookup_splitting |> HOLogic.mk_list @{typ nat} - |> Thm.cterm_of (ProofContext.theory_of ctxt) + |> Thm.cterm_of (Proof_Context.theory_of ctxt) in (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n), (@{cpat "?prec::nat"}, p), @@ -3388,9 +3388,9 @@ else let val t = t |> HOLogic.mk_number @{typ nat} - |> Thm.cterm_of (ProofContext.theory_of ctxt) + |> Thm.cterm_of (Proof_Context.theory_of ctxt) val s = vs |> map lookup_splitting |> hd - |> Thm.cterm_of (ProofContext.theory_of ctxt) + |> Thm.cterm_of (Proof_Context.theory_of ctxt) in rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s), (@{cpat "?t::nat"}, t), @@ -3530,9 +3530,9 @@ fun approx_form prec ctxt t = realify t - |> prepare_form (ProofContext.theory_of ctxt) + |> prepare_form (Proof_Context.theory_of ctxt) |> (fn arith_term => - reify_form (ProofContext.theory_of ctxt) arith_term + reify_form (Proof_Context.theory_of ctxt) arith_term |> HOLogic.dest_Trueprop |> dest_interpret_form |> (fn (data, xs) => mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"} diff -r da8817d01e7c -r 23f352990944 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Sat Apr 16 16:15:37 2011 +0200 @@ -1996,7 +1996,7 @@ let val vs = Term.add_frees t []; val t' = (term_of_fm vs o @{code linrqe} o fm_of_term vs) t; - in (Thm.cterm_of (ProofContext.theory_of ctxt) o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end + in (Thm.cterm_of (Proof_Context.theory_of ctxt) o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end end; *} diff -r da8817d01e7c -r 23f352990944 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Apr 16 16:15:37 2011 +0200 @@ -3012,7 +3012,7 @@ THEN (fn st => let val g = List.nth (cprems_of st, i - 1) - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps val th = frpar_oracle (T, fs,ps, (* Pattern.eta_long [] *)g) in rtac (th RS iffD2) i st end); @@ -3022,7 +3022,7 @@ THEN (fn st => let val g = List.nth (cprems_of st, i - 1) - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps val th = frpar_oracle2 (T, fs,ps, (* Pattern.eta_long [] *)g) in rtac (th RS iffD2) i st end); diff -r da8817d01e7c -r 23f352990944 src/HOL/Decision_Procs/commutative_ring_tac.ML --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML Sat Apr 16 16:15:37 2011 +0200 @@ -86,7 +86,7 @@ fun tac ctxt = SUBGOAL (fn (g, i) => let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*) addsimps cring_simps; val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g) diff -r da8817d01e7c -r 23f352990944 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Apr 16 16:15:37 2011 +0200 @@ -69,7 +69,7 @@ fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st => let val g = List.nth (prems_of st, i - 1) - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_linz q g (* Some simpsets for dealing with mod div abs and nat*) diff -r da8817d01e7c -r 23f352990944 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sat Apr 16 16:15:37 2011 +0200 @@ -77,7 +77,7 @@ THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}]) THEN' SUBGOAL (fn (g, i) => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_linr thy q g (* Some simpsets for dealing with mod div abs and nat*) diff -r da8817d01e7c -r 23f352990944 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Apr 16 16:15:37 2011 +0200 @@ -94,7 +94,7 @@ THEN (fn st => let val g = List.nth (prems_of st, i - 1) - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_mir thy q g (* Some simpsets for dealing with mod div abs and nat*) diff -r da8817d01e7c -r 23f352990944 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/HOL.thy Sat Apr 16 16:15:37 2011 +0200 @@ -1262,7 +1262,7 @@ then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) else let (*Norbert Schirmer's case*) val ctxt = Simplifier.the_context ss; - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val t = Thm.term_of ct; val ([t'], ctxt') = Variable.import_terms false [t] ctxt; in Option.map (hd o Variable.export ctxt' ctxt o single) @@ -1612,7 +1612,7 @@ fun proc phi ss ct = let val ctxt = Simplifier.the_context ss; - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; in case Thm.term_of ct of (_ $ t $ u) => if matches thy u then NONE else SOME meta_reorient @@ -1964,12 +1964,12 @@ subsubsection {* Evaluation and normalization by evaluation *} setup {* - Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) (* FIXME proper context!? *) + Value.add_evaluator ("SML", Codegen.eval_term o Proof_Context.theory_of) (* FIXME proper context!? *) *} ML {* fun gen_eval_method conv ctxt = SIMPLE_METHOD' - (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) (conv (ProofContext.theory_of ctxt)))) ctxt) + (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) (conv (Proof_Context.theory_of ctxt)))) ctxt) THEN' rtac TrueI) *} @@ -1981,7 +1981,7 @@ method_setup normalization = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' - (CHANGED_PROP o (CONVERSION (Nbe.dynamic_conv (ProofContext.theory_of ctxt)) + (CHANGED_PROP o (CONVERSION (Nbe.dynamic_conv (Proof_Context.theory_of ctxt)) THEN' (fn k => TRY (rtac TrueI k))))) *} "solve goal by normalization" diff -r da8817d01e7c -r 23f352990944 src/HOL/HOLCF/Tools/Domain/domain.ML --- a/src/HOL/HOLCF/Tools/Domain/domain.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Sat Apr 16 16:15:37 2011 +0200 @@ -193,7 +193,7 @@ (* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *) fun read_typ thy sorts str = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy |> fold (Variable.declare_typ o TFree) sorts in Syntax.read_typ ctxt str end diff -r da8817d01e7c -r 23f352990944 src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sat Apr 16 16:15:37 2011 +0200 @@ -225,7 +225,7 @@ in bot :: map name_of (#con_specs constr_info) end in adms @ flat (map2 one_eq bottoms constr_infos) end - val inducts = Project_Rule.projections (ProofContext.init_global thy) ind + val inducts = Project_Rule.projections (Proof_Context.init_global thy) ind fun ind_rule (dname, rule) = ((Binding.empty, rule), [Rule_Cases.case_names case_ns, Induct.induct_type dname]) diff -r da8817d01e7c -r 23f352990944 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Apr 16 16:15:37 2011 +0200 @@ -177,7 +177,7 @@ val cont_thm = let val prop = mk_trp (mk_cont functional) - val rules = Cont2ContData.get (ProofContext.init_global thy) + val rules = Cont2ContData.get (Proof_Context.init_global thy) val tac = REPEAT_ALL_NEW (match_tac rules) 1 in Goal.prove_global thy [] [] prop (K tac) @@ -185,7 +185,7 @@ val tuple_unfold_thm = (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm]) - |> Local_Defs.unfold (ProofContext.init_global thy) @{thms split_conv} + |> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv} fun mk_unfold_thms [] thm = [] | mk_unfold_thms (n::[]) thm = [(n, thm)] @@ -214,7 +214,7 @@ (tab2 : (typ * term) list) (T : typ) : term = let - val defl_simps = RepData.get (ProofContext.init_global thy) + val defl_simps = RepData.get (Proof_Context.init_global thy) val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2 fun proc1 t = @@ -389,7 +389,7 @@ fun read_typ thy str sorts = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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 @@ -541,7 +541,7 @@ fun mk_DEFL_eq_thm (lhsT, rhsT) = let val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT) - val DEFL_simps = RepData.get (ProofContext.init_global thy) + val DEFL_simps = RepData.get (Proof_Context.init_global thy) val tac = rewrite_goals_tac (map mk_meta_eq DEFL_simps) THEN TRY (resolve_tac defl_unfold_thms 1) @@ -647,7 +647,7 @@ val isodefl_rules = @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL} @ isodefl_abs_rep_thms - @ IsodeflData.get (ProofContext.init_global thy) + @ IsodeflData.get (Proof_Context.init_global thy) in Goal.prove_global thy [] assms goal (fn {prems, ...} => EVERY diff -r da8817d01e7c -r 23f352990944 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Apr 16 16:15:37 2011 +0200 @@ -142,10 +142,10 @@ Context.theory_map (DeflMapData.add_thm thm) val get_rec_tab = Rec_Data.get -fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy) +fun get_deflation_thms thy = DeflMapData.get (Proof_Context.init_global thy) val map_ID_add = Map_Id_Data.add -val get_map_ID_thms = Map_Id_Data.get o ProofContext.init_global +val get_map_ID_thms = Map_Id_Data.get o Proof_Context.init_global val setup = DeflMapData.setup #> Map_Id_Data.setup diff -r da8817d01e7c -r 23f352990944 src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Sat Apr 16 16:15:37 2011 +0200 @@ -163,7 +163,7 @@ (*rhs*) val tmp_ctxt = - ProofContext.init_global thy + Proof_Context.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 @@ -173,7 +173,7 @@ error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT)) (*lhs*) - val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args + val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt') raw_args val full_tname = Sign.full_name thy tname val newT = Type (full_tname, map TFree lhs_tfrees) @@ -199,8 +199,8 @@ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po}) |> Specification.definition (NONE, ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn)) - val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy) - val below_def = singleton (ProofContext.export lthy ctxt_thy) below_ldef + val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy) + val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef val thy = lthy |> Class.prove_instantiation_exit (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1)) @@ -313,22 +313,22 @@ fun gen_cpodef_proof prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) thy = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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 - fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) + fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) | after_qed _ = raise Fail "cpodef_proof" in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end fun gen_pcpodef_proof prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) thy = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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 - fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) + fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) | after_qed _ = raise Fail "pcpodef_proof" in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end diff -r da8817d01e7c -r 23f352990944 src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Sat Apr 16 16:15:37 2011 +0200 @@ -93,7 +93,7 @@ (*rhs*) val tmp_ctxt = - ProofContext.init_global thy + Proof_Context.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 @@ -103,7 +103,7 @@ else error ("Not type defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT)) (*lhs*) - val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args + val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt) raw_args val lhs_sorts = map snd lhs_tfrees val full_tname = Sign.full_name thy tname val newT = Type (full_tname, map TFree lhs_tfrees) @@ -161,13 +161,13 @@ Specification.definition (NONE, (liftprj_bind, liftprj_eqn)) lthy val ((_, (_, liftdefl_ldef)), lthy) = Specification.definition (NONE, (liftdefl_bind, liftdefl_eqn)) 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 defl_def = singleton (ProofContext.export lthy ctxt_thy) defl_ldef - val liftemb_def = singleton (ProofContext.export lthy ctxt_thy) liftemb_ldef - val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef - val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef + val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy) + val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef + val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef + val defl_def = singleton (Proof_Context.export lthy ctxt_thy) defl_ldef + val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef + val liftprj_def = singleton (Proof_Context.export lthy ctxt_thy) liftprj_ldef + val liftdefl_def = singleton (Proof_Context.export lthy ctxt_thy) liftdefl_ldef val type_definition_thm = Raw_Simplifier.rewrite_rule (the_list (#set_def (#2 info))) @@ -208,7 +208,7 @@ fun domaindef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args in snd (gen_add_domaindef Syntax.read_term def name (b, args, mx) A morphs thy) end diff -r da8817d01e7c -r 23f352990944 src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Sat Apr 16 16:15:37 2011 +0200 @@ -122,7 +122,7 @@ (spec : (Attrib.binding * term) list) (lthy : local_theory) = let - val thy = ProofContext.theory_of lthy + val thy = Proof_Context.theory_of lthy val names = map (Binding.name_of o fst o fst) fixes val all_names = space_implode "_" names val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec) @@ -355,7 +355,7 @@ (all_names ~~ (spec ~~ skips)) val blocks = map block_of_name names - val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy) + val matcher_tab = FixrecMatchData.get (Proof_Context.theory_of lthy) fun match_name c = case Symtab.lookup matcher_tab c of SOME m => m | NONE => fixrec_err ("unknown pattern constructor: " ^ c) diff -r da8817d01e7c -r 23f352990944 src/HOL/Import/import.ML --- a/src/HOL/Import/import.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Import/import.ML Sat Apr 16 16:15:37 2011 +0200 @@ -25,11 +25,11 @@ fun import_tac ctxt (thyname, thmname) = if ! quick_and_dirty - then Skip_Proof.cheat_tac (ProofContext.theory_of ctxt) + then Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt) else fn th => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val prem = hd (prems_of th) val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname) val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem) diff -r da8817d01e7c -r 23f352990944 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Import/shuffler.ML Sat Apr 16 16:15:37 2011 +0200 @@ -608,7 +608,7 @@ fun gen_shuffle_tac ctxt search thms i st = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val _ = message ("Shuffling " ^ (string_of_thm st)) val t = List.nth(prems_of st,i-1) val set = set_prop thy t diff -r da8817d01e7c -r 23f352990944 src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML Sat Apr 16 16:15:37 2011 +0200 @@ -98,7 +98,7 @@ val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >> - (fn (x, k) => (cterm_of (ProofContext.theory_of ctxt) (Free (x, @{typ real})), k)) + (fn (x, k) => (cterm_of (Proof_Context.theory_of ctxt) (Free (x, @{typ real})), k)) fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >> (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty) diff -r da8817d01e7c -r 23f352990944 src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Library/reflection.ML Sat Apr 16 16:15:37 2011 +0200 @@ -33,7 +33,7 @@ let val (f as Const(fN,fT)) = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> strip_comb |> fst - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val cert = Thm.cterm_of thy val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th')) @@ -118,7 +118,7 @@ constructor and n is the number of the atom corresponding to t *) fun decomp_genreif da cgns (t,ctxt) bds = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val cert = cterm_of thy fun tryabsdecomp (s,ctxt) bds = (case s of @@ -192,7 +192,7 @@ (insert (op aconv) vs vss, insert (op aconv) n ns)) nths ([],[]) val (vsns, ctxt') = Variable.variant_fixes (replicate (length vss) "vs") ctxt val (xns, ctxt'') = Variable.variant_fixes (replicate (length nths) "x") ctxt' - val thy = ProofContext.theory_of ctxt'' + val thy = Proof_Context.theory_of ctxt'' val cert = cterm_of thy val certT = ctyp_of thy val vsns_map = vss ~~ vsns @@ -247,7 +247,7 @@ val tys = fold_rev (fn f => fold (insert (op =)) (f |> fastype_of |> binder_types |> tl) ) fs [] val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt - val thy = ProofContext.theory_of ctxt' + val thy = Proof_Context.theory_of ctxt' val cert = cterm_of thy val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t))))) (tys ~~ vs) @@ -274,7 +274,7 @@ | is_listVar _ = false val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd |> strip_comb |> snd |> filter is_listVar - val cert = cterm_of (ProofContext.theory_of ctxt) + val cert = cterm_of (Proof_Context.theory_of ctxt) val cvs = map (fn (v as Var(n,t)) => (cert v, the (AList.lookup Type.could_unify bds t) |> snd |> HOLogic.mk_list (dest_listT t) |> cert)) vars val th' = instantiate ([], cvs) th diff -r da8817d01e7c -r 23f352990944 src/HOL/List.thy --- a/src/HOL/List.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/List.thy Sat Apr 16 16:15:37 2011 +0200 @@ -395,8 +395,8 @@ fun abs_tr ctxt (p as Free (s, T)) e opti = let - val thy = ProofContext.theory_of ctxt; - val s' = ProofContext.intern_const ctxt s; + val thy = Proof_Context.theory_of ctxt; + val s' = Proof_Context.intern_const ctxt s; in if Sign.declared_const thy s' then (pat_tr ctxt p e opti, false) diff -r da8817d01e7c -r 23f352990944 src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Sat Apr 16 16:15:37 2011 +0200 @@ -16,7 +16,7 @@ val names = map Thm.get_name_hint thms val add_info = if null names then I else suffix (":\n" ^ commas names) - val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre)) + val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) fun metis ctxt = Metis_Tactics.metis_tac ctxt (thms @ facts) in diff -r da8817d01e7c -r 23f352990944 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Apr 16 16:15:37 2011 +0200 @@ -411,7 +411,7 @@ fun thms_of_name ctxt name = let val lex = Keyword.get_lexicons - val get = maps (ProofContext.get_fact ctxt o fst) + val get = maps (Proof_Context.get_fact ctxt o fst) in Source.of_string name |> Symbol.source diff -r da8817d01e7c -r 23f352990944 src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Sat Apr 16 16:15:37 2011 +0200 @@ -331,7 +331,7 @@ fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r - val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns + val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (Proof_Context.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns val replace_conv = try_conv (rewrs_conv asl) val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) val ges' = diff -r da8817d01e7c -r 23f352990944 src/HOL/Mutabelle/Mutabelle.thy --- a/src/HOL/Mutabelle/Mutabelle.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Mutabelle/Mutabelle.thy Sat Apr 16 16:15:37 2011 +0200 @@ -61,16 +61,16 @@ (* ML {* -Quickcheck.test_term (ProofContext.init_global @{theory}) +Quickcheck.test_term (Proof_Context.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_global thy) false (SOME "SML") 1 1) (prop_of th); + (Proof_Context.init_global thy) false (SOME "SML") 1 1) (prop_of th); fun is_executable_term thy t = can (Quickcheck.test_term - (ProofContext.init_global thy) false (SOME "SML") 1 1) t; + (Proof_Context.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 da8817d01e7c -r 23f352990944 src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle.ML Sat Apr 16 16:15:37 2011 +0200 @@ -496,7 +496,7 @@ fun is_executable thy insts th = ((Quickcheck.test_term - (ProofContext.init_global thy + (Proof_Context.init_global thy |> Config.put Quickcheck.size 1 |> Config.put Quickcheck.iterations 1 |> Config.put Quickcheck.tester (!testgen_name)) @@ -510,7 +510,7 @@ ((x, pretty (the_default [] (Quickcheck.counterexample_of (Quickcheck.test_term ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter #> Config.put Quickcheck.tester (!testgen_name)) - (ProofContext.init_global usedthy)) + (Proof_Context.init_global usedthy)) (true, false) (preprocess usedthy insts x, []))))) :: acc)) handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc); diff -r da8817d01e7c -r 23f352990944 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Apr 16 16:15:37 2011 +0200 @@ -122,7 +122,7 @@ TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit)) (fn _ => let - val [result] = Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy)) + val [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy)) (false, false) [] [(t, [])] in case Quickcheck.counterexample_of result of @@ -139,7 +139,7 @@ fun invoke_solve_direct thy t = let - val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) + val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) in case Solve_Direct.solve_direct false state of (true, _) => (Solved, []) @@ -152,7 +152,7 @@ fun invoke_try thy t = let - val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) + val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy) in case Try.invoke_try (SOME (seconds 5.0)) ([], [], [], []) state of true => (Solved, []) @@ -196,7 +196,7 @@ fun invoke_nitpick thy t = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy val state = Proof.init ctxt val (res, _) = Nitpick.pick_nits_in_term state (Nitpick_Isar.default_params thy []) false 1 1 1 [] [] t @@ -312,7 +312,7 @@ fun is_executable_term thy t = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy in can (TimeLimit.timeLimit (seconds 2.0) (Quickcheck.test_goal_terms @@ -414,7 +414,7 @@ (* |> filter (not o is_forbidden_mutant) *) |> List.mapPartial (try (Sign.cert_term thy)) |> List.filter (is_some o try (Thm.cterm_of thy)) - |> List.filter (is_some o try (Syntax.check_term (ProofContext.init_global thy))) + |> List.filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy))) |> take_random max_mutants val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants in @@ -490,7 +490,7 @@ fun mutate_theorems_and_write_report thy mtds thms file_name = let val _ = Output.urgent_message "Starting Mutabelle..." - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy val path = Path.explode file_name (* for normal report: *) (* diff -r da8817d01e7c -r 23f352990944 src/HOL/NSA/transfer.ML --- a/src/HOL/NSA/transfer.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/NSA/transfer.ML Sat Apr 16 16:15:37 2011 +0200 @@ -53,7 +53,7 @@ fun transfer_thm_of ctxt ths t = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt); val meta = Local_Defs.meta_rewrite_rule ctxt; val ths' = map meta ths; diff -r da8817d01e7c -r 23f352990944 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Apr 16 16:15:37 2011 +0200 @@ -149,7 +149,7 @@ Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \ (pi2 \ x)"] perm_simproc'; fun projections rule = - Project_Rule.projections (ProofContext.init_global (Thm.theory_of_thm rule)) rule + Project_Rule.projections (Proof_Context.init_global (Thm.theory_of_thm rule)) rule |> map (Drule.export_without_context #> Rule_Cases.save rule); val supp_prod = @{thm supp_prod}; @@ -1374,7 +1374,7 @@ resolve_tac freshs2' i | _ => asm_simp_tac (HOL_basic_ss addsimps pt2_atoms addsimprocs [perm_simproc]) i)) 1]) - val final = ProofContext.export context3 context2 [th] + val final = Proof_Context.export context3 context2 [th] in resolve_tac final 1 end) context1 1) (constrs ~~ constrs')) (descr'' ~~ ndescr))) @@ -1615,7 +1615,7 @@ val y = Free ("y", U); val y' = Free ("y'", U) in - Drule.export_without_context (Goal.prove (ProofContext.init_global thy11) [] + Drule.export_without_context (Goal.prove (Proof_Context.init_global thy11) [] (map (augment_sort thy11 fs_cp_sort) (finite_prems @ [HOLogic.mk_Trueprop (R $ x $ y), @@ -1710,7 +1710,7 @@ (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs; val rec_unique_thms = split_conj_thm (Goal.prove - (ProofContext.init_global thy11) (map fst rec_unique_frees) + (Proof_Context.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 @@ -1993,7 +1993,7 @@ (fn _ => cut_facts_tac [pi1_pi2_result RS sym] 1 THEN full_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh @ fresh_results @ fresh_results') 1); - val final' = ProofContext.export context'' context' [final]; + val final' = Proof_Context.export context'' context' [final]; val _ = warning "finished!" in resolve_tac final' 1 diff -r da8817d01e7c -r 23f352990944 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sat Apr 16 16:15:37 2011 +0200 @@ -125,7 +125,7 @@ (* Find the variable we instantiate *) let val thy = theory_of_thm thm; - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; val ss = global_simpset_of thy; val abs_fresh = Global_Theory.get_thms thy "abs_fresh"; val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app"; diff -r da8817d01e7c -r 23f352990944 src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Nominal/nominal_induct.ML Sat Apr 16 16:15:37 2011 +0200 @@ -54,7 +54,7 @@ end; val substs = map2 subst insts concls |> flat |> distinct (op =) - |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt))); + |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt))); in (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) end; @@ -83,7 +83,7 @@ fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val cert = Thm.cterm_of thy; val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; @@ -92,7 +92,7 @@ val finish_rule = split_all_tuples #> rename_params_rule true - (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding); + (map (Name.clean o Proof_Context.revert_skolem defs_ctxt o fst) avoiding); fun rule_cases ctxt r = let val r' = if simp then Induct.simplified_rule ctxt r else r @@ -126,7 +126,7 @@ |> Seq.maps (fn rule' => CASES (rule_cases ctxt rule' cases) (Tactic.rtac (rename_params_rule false [] rule') i THEN - PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) + PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) THEN_ALL_NEW_CASES ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac) else K all_tac) diff -r da8817d01e7c -r 23f352990944 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Sat Apr 16 16:15:37 2011 +0200 @@ -146,7 +146,7 @@ fun prove_strong_ind s avoids ctxt = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val ({names, ...}, {raw_induct, intrs, elims, ...}) = Inductive.the_inductive ctxt (Sign.intern_const thy s); val ind_params = Inductive.params_of raw_induct; @@ -396,7 +396,7 @@ (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss addsimps vc_compat_ths'' @ freshs2' @ perm_fresh_fresh @ fresh_atm) 1); - val final' = ProofContext.export ctxt'' ctxt' [final]; + val final' = Proof_Context.export ctxt'' ctxt' [final]; in resolve_tac final' 1 end) context 1]) (prems ~~ thss ~~ ihyps ~~ prems''))) in @@ -404,7 +404,7 @@ REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN asm_full_simp_tac (simpset_of ctxt) 1) - end) |> singleton (ProofContext.export ctxt' ctxt); + end) |> singleton (Proof_Context.export ctxt' ctxt); (** strong case analysis rule **) @@ -536,10 +536,10 @@ REPEAT_DETERM (TRY (rtac conjI 1) THEN resolve_tac case_hyps' 1) end) ctxt4 1) - val final = ProofContext.export ctxt3 ctxt2 [th] + val final = Proof_Context.export ctxt3 ctxt2 [th] in resolve_tac final 1 end) ctxt1 1) (thss ~~ hyps ~~ prems))) |> - singleton (ProofContext.export ctxt' ctxt)) + singleton (Proof_Context.export ctxt' ctxt)) in ctxt'' |> @@ -584,7 +584,7 @@ fun prove_eqvt s xatoms ctxt = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val ({names, ...}, {raw_induct, intrs, elims, ...}) = Inductive.the_inductive ctxt (Sign.intern_const thy s); val raw_induct = atomize_induct ctxt raw_induct; @@ -659,7 +659,7 @@ (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs => full_simp_tac eqvt_ss 1 THEN eqvt_tac context pi' intr_vs) intrs')) |> - singleton (ProofContext.export ctxt' ctxt))) + singleton (Proof_Context.export ctxt' ctxt))) end) atoms in ctxt |> diff -r da8817d01e7c -r 23f352990944 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Apr 16 16:15:37 2011 +0200 @@ -153,7 +153,7 @@ fun prove_strong_ind s alt_name avoids ctxt = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val ({names, ...}, {raw_induct, intrs, elims, ...}) = Inductive.the_inductive ctxt (Sign.intern_const thy s); val ind_params = Inductive.params_of raw_induct; @@ -182,7 +182,7 @@ | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs)); fun mk_avoids params name sets = let - val (_, ctxt') = ProofContext.add_fixes + val (_, ctxt') = Proof_Context.add_fixes (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt; fun mk s = let @@ -311,7 +311,7 @@ fun obtain_fresh_name ts sets (T, fin) (freshs, ths1, ths2, ths3, ctxt) = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; (** protect terms to avoid that fresh_star_prod_set interferes with **) (** pairs used in introduction rules of inductive predicate **) fun protect t = @@ -432,7 +432,7 @@ (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss addsimps vc_compat_ths1' @ fresh_ths1 @ perm_freshs_freshs') 1); - val final' = ProofContext.export ctxt'' ctxt' [final]; + val final' = Proof_Context.export ctxt'' ctxt' [final]; in resolve_tac final' 1 end) context 1]) (prems ~~ thss ~~ vc_compat' ~~ ihyps ~~ prems''))) in @@ -442,7 +442,7 @@ asm_full_simp_tac (simpset_of ctxt) 1) end) |> fresh_postprocess |> - singleton (ProofContext.export ctxt' ctxt); + singleton (Proof_Context.export ctxt' ctxt); in ctxt'' |> diff -r da8817d01e7c -r 23f352990944 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Sat Apr 16 16:15:37 2011 +0200 @@ -247,7 +247,7 @@ val eqns' = map unquantify spec' val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) spec' []; - val dt_info = NominalDatatype.get_nominal_datatypes (ProofContext.theory_of lthy); + val dt_info = NominalDatatype.get_nominal_datatypes (Proof_Context.theory_of lthy); val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) => map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns val _ = @@ -284,7 +284,7 @@ val qualify = Binding.qualify false (space_implode "_" (map (Long_Name.base_name o #1) defs)); val names_atts' = map (apfst qualify) names_atts; - val cert = cterm_of (ProofContext.theory_of lthy'); + val cert = cterm_of (Proof_Context.theory_of lthy'); fun mk_idx eq = let @@ -366,7 +366,7 @@ Proof.theorem NONE (fn thss => fn goal_ctxt => let - val simps = ProofContext.export goal_ctxt lthy' (flat thss); + val simps = Proof_Context.export goal_ctxt lthy' (flat thss); val (simps', lthy'') = fold_map Local_Theory.note (names_atts' ~~ map single simps) lthy'; in diff -r da8817d01e7c -r 23f352990944 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Sat Apr 16 16:15:37 2011 +0200 @@ -52,7 +52,7 @@ fun prove_eqvt_tac ctxt orig_thm pi pi' = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val mypi = Thm.cterm_of thy pi val T = fastype_of pi' val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi') @@ -70,7 +70,7 @@ fun get_derived_thm ctxt hyp concl orig_thm pi typi = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val pi' = Var (pi, typi); val lhs = Const (@{const_name "perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp; val ([goal_term, pi''], ctxt') = Variable.import_terms false @@ -79,7 +79,7 @@ in Goal.prove ctxt' [] [] goal_term (fn _ => prove_eqvt_tac ctxt' orig_thm pi' pi'') |> - singleton (ProofContext.export ctxt' ctxt) + singleton (Proof_Context.export ctxt' ctxt) end (* replaces in t every variable, say x, with pi o x *) diff -r da8817d01e7c -r 23f352990944 src/HOL/SPARK/Tools/spark_commands.ML --- a/src/HOL/SPARK/Tools/spark_commands.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Sat Apr 16 16:15:37 2011 +0200 @@ -32,7 +32,7 @@ end; fun add_proof_fun_cmd pf thy = - let val ctxt = ProofContext.init_global thy + let val ctxt = Proof_Context.init_global thy in SPARK_VCs.add_proof_fun (fn optT => Syntax.parse_term ctxt #> the_default I (Option.map Type.constraint optT) #> @@ -54,7 +54,7 @@ fun prove_vc vc_name lthy = let - val thy = ProofContext.theory_of lthy; + val thy = Proof_Context.theory_of lthy; val (ctxt, stmt) = get_vc thy vc_name in Specification.theorem Thm.theoremK NONE @@ -80,7 +80,7 @@ val ctxt = state |> Toplevel.theory_of |> - ProofContext.init_global |> + Proof_Context.init_global |> Context.proof_map (fold Element.init context) in [Pretty.str "Context:", diff -r da8817d01e7c -r 23f352990944 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Apr 16 16:15:37 2011 +0200 @@ -95,7 +95,7 @@ | mk_type thy ty = (case get_type thy ty of NONE => - Syntax.check_typ (ProofContext.init_global thy) + Syntax.check_typ (Proof_Context.init_global thy) (Type (Sign.full_name thy (Binding.name ty), [])) | SOME T => T); @@ -108,8 +108,8 @@ Logic.dest_equals |>> dest_Free; val ((_, (_, thm)), lthy') = Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy - val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy'); - val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm + val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy'); + val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm in (thm', lthy') end; fun strip_underscores s = @@ -183,7 +183,7 @@ rtac @{thm subset_antisym} 1 THEN rtac @{thm subsetI} 1 THEN Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info - (ProofContext.theory_of lthy) tyname'))) 1 THEN + (Proof_Context.theory_of lthy) tyname'))) 1 THEN ALLGOALS (asm_full_simp_tac (simpset_of lthy))); val finite_UNIV = Goal.prove lthy [] [] @@ -904,7 +904,7 @@ val ((t', (_, th)), lthy') = Specification.definition (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)))) lthy; - val phi = ProofContext.export_morphism lthy' lthy + val phi = Proof_Context.export_morphism lthy' lthy in ((id', Morphism.thm phi th), ((Symtab.update (s, (Morphism.term phi t', ty)) tab, diff -r da8817d01e7c -r 23f352990944 src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sat Apr 16 16:15:37 2011 +0200 @@ -334,7 +334,7 @@ fun neq_x_y ctxt x y name = (let - val dist_thm = the (try (ProofContext.get_thm ctxt) name); + val dist_thm = the (try (Proof_Context.get_thm ctxt) name); val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; val tree = term_of ctree; val x_path = the (find_tree x tree); diff -r da8817d01e7c -r 23f352990944 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Statespace/state_space.ML Sat Apr 16 16:15:37 2011 +0200 @@ -148,7 +148,7 @@ |> Expression.sublocale_cmd I name expr [] |> Proof.global_terminal_proof (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE) - |> ProofContext.theory_of + |> Proof_Context.theory_of fun add_locale name expr elems thy = thy @@ -197,7 +197,7 @@ if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name then let val n' = lookupI (op =) (Variable.fixes_of ctxt) name - in SOME (Free (n',ProofContext.infer_type ctxt (n', dummyT))) end + in SOME (Free (n',Proof_Context.infer_type ctxt (n', dummyT))) end else NONE @@ -251,7 +251,7 @@ fun solve_tac ctxt (_,i) st = let - val distinct_thm = ProofContext.get_thm ctxt dist_thm_name; + val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name; val goal = List.nth (cprems_of st,i-1); val rule = DistinctTreeProver.distinct_implProver distinct_thm goal; in EVERY [rtac rule i] st @@ -312,7 +312,7 @@ ([]))])]; in thy |> add_locale name ([],vars) [assumes] - |> ProofContext.theory_of + |> Proof_Context.theory_of |> interprete_parent name dist_thm_full_name parent_expr end; @@ -428,7 +428,7 @@ let fun upd (n,v) = let - val nT = ProofContext.infer_type (Local_Theory.target_of lthy) (n, dummyT) + val nT = Proof_Context.infer_type (Local_Theory.target_of lthy) (n, dummyT) in Context.proof_map (update_declinfo (Morphism.term phi (Free (n,nT)),v)) end; @@ -458,12 +458,12 @@ (map fst parent_comps) (map fst components) |> Context.theory_map (add_statespace full_name args parents components []) |> add_locale (suffix valuetypesN name) (locinsts,locs) [] - |> ProofContext.theory_of + |> Proof_Context.theory_of |> fold interprete_parent_valuetypes parents |> add_locale_cmd name ([(suffix namespaceN full_name ,(("",false),Expression.Named [])), (suffix valuetypesN full_name,(("",false),Expression.Named []))],[]) fixestate - |> ProofContext.theory_of + |> Proof_Context.theory_of |> fold interprete_parent parents |> add_declaration full_name (declare_declinfo components') end; @@ -472,7 +472,7 @@ (* prepare arguments *) fun read_raw_parent ctxt raw_T = - (case ProofContext.read_typ_abbrev ctxt raw_T of + (case Proof_Context.read_typ_abbrev ctxt raw_T of Type (name, Ts) => (Ts, name) | T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T)); @@ -485,7 +485,7 @@ fun cert_typ ctxt raw_T env = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg; val env' = OldTerm.add_typ_tfrees (T, env); @@ -500,7 +500,7 @@ *) val _ = writeln ("Defining statespace " ^ quote name ^ " ..."); - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; fun add_parent (Ts,pname,rs) env = let diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Sat Apr 16 16:15:37 2011 +0200 @@ -297,7 +297,7 @@ end; fun make_case tab ctxt = gen_make_case - (match_type (ProofContext.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt; + (match_type (Proof_Context.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt; val make_case_untyped = gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT); @@ -306,8 +306,8 @@ fun case_tr err tab_of ctxt [t, u] = let - val thy = ProofContext.theory_of ctxt; - val intern_const_syntax = Consts.intern_syntax (ProofContext.consts_of ctxt); + val thy = Proof_Context.theory_of ctxt; + val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt); (* replace occurrences of dummy_pattern by distinct variables *) (* internalize constant names *) @@ -320,7 +320,7 @@ | prep_pat (Const (s, T)) used = (Const (intern_const_syntax s, T), used) | prep_pat (v as Free (s, T)) used = - let val s' = ProofContext.intern_const ctxt s in + let val s' = Proof_Context.intern_const ctxt s in if Sign.declared_const thy s' then (Const (s', T), used) else (v, used) @@ -449,7 +449,7 @@ fun case_tr' tab_of cname ctxt ts = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; fun mk_clause (pat, rhs) = let val xs = Term.add_frees pat [] in Syntax.const @{syntax_const "_case1"} $ diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Sat Apr 16 16:15:37 2011 +0200 @@ -100,11 +100,11 @@ val def' = Syntax.check_term lthy def; val ((_, (_, thm)), lthy') = Specification.definition (NONE, (Attrib.empty_binding, def')) lthy; - val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); - val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm; + val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); + val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm; in (thm', lthy') end; fun tac thms = Class.intro_classes_tac [] - THEN ALLGOALS (ProofContext.fact_tac thms); + THEN ALLGOALS (Proof_Context.fact_tac thms); fun prefix tyco = Binding.qualify true (Long_Name.base_name tyco) o Binding.qualify true "eq" o Binding.name; fun add_eq_thms tyco = Theory.checkpoint diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Sat Apr 16 16:15:37 2011 +0200 @@ -166,7 +166,7 @@ fun read_typ thy str sorts = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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; @@ -216,10 +216,10 @@ (* translation rules for case *) fun make_case ctxt = Datatype_Case.make_case - (info_of_constr (ProofContext.theory_of ctxt)) ctxt; + (info_of_constr (Proof_Context.theory_of ctxt)) ctxt; fun strip_case ctxt = Datatype_Case.strip_case - (info_of_case (ProofContext.theory_of ctxt)); + (info_of_case (Proof_Context.theory_of ctxt)); fun add_case_tr' case_names thy = Sign.add_advanced_trfuns ([], [], @@ -240,7 +240,7 @@ val _ = Thy_Output.antiquotation "datatype" (Args.type_name true) (fn {source = src, context = ctxt, ...} => fn dtco => let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val (vs, cos) = the_spec thy dtco; val ty = Type (dtco, map TFree vs); val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt); @@ -318,7 +318,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_global thy2) induct; + val inducts = Project_Rule.projections (Proof_Context.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 ~~ @@ -378,12 +378,12 @@ fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; fun constr_of_term (Const (c, T)) = (c, T) | constr_of_term t = error ("Not a constant: " ^ Syntax.string_of_term ctxt t); fun no_constr (c, T) = - error ("Bad constructor: " ^ ProofContext.extern_const ctxt c ^ "::" ^ + error ("Bad constructor: " ^ Proof_Context.extern_const ctxt c ^ "::" ^ Syntax.string_of_typ ctxt T); fun type_of_constr (cT as (_, T)) = let @@ -432,7 +432,7 @@ unflat rules (map Drule.zero_var_indexes_list raw_thms); (*FIXME somehow dubious*) in - ProofContext.background_theory_result + Proof_Context.background_theory_result (prove_rep_datatype config dt_names alt_names descr vs raw_inject half_distinct raw_induct) #-> after_qed diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/context_tree.ML --- a/src/HOL/Tools/Function/context_tree.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/context_tree.ML Sat Apr 16 16:15:37 2011 +0200 @@ -111,12 +111,12 @@ fun find_cong_rule ctx fvar h ((r,dep)::rs) t = (let - val thy = ProofContext.theory_of ctx + val thy = Proof_Context.theory_of ctx val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t) val (c, subs) = (concl_of r, prems_of r) - val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty) + val subst = Pattern.match (Proof_Context.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty) val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c []) @@ -147,7 +147,7 @@ val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t fun subtree (ctx', fixes, assumes, st) = ((fixes, - map (Thm.assume o cterm_of (ProofContext.theory_of ctx)) assumes), + map (Thm.assume o cterm_of (Proof_Context.theory_of ctx)) assumes), mk_tree' ctx' st) in Cong (r, dep, map subtree branches) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/fun.ML --- a/src/HOL/Tools/Function/fun.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/fun.ML Sat Apr 16 16:15:37 2011 +0200 @@ -29,7 +29,7 @@ fun err str = error (cat_lines ["Malformed definition:", str ^ " not allowed in sequential mode.", Syntax.string_of_term ctxt geq]) - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun check_constr_pattern (Bound _) = () | check_constr_pattern t = diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/function.ML Sat Apr 16 16:15:37 2011 +0200 @@ -231,11 +231,11 @@ val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy in lthy - |> ProofContext.note_thmss "" + |> Proof_Context.note_thmss "" [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd - |> ProofContext.note_thmss "" + |> Proof_Context.note_thmss "" [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd - |> ProofContext.note_thmss "" + |> Proof_Context.note_thmss "" [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), [([Goal.norm_result termination], [])])] |> snd |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]] diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/function_common.ML Sat Apr 16 16:15:37 2011 +0200 @@ -127,7 +127,7 @@ fun import_function_data t ctxt = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ct = cterm_of thy t val inst_morph = lift_morphism thy o Thm.instantiate @@ -277,7 +277,7 @@ plural " " "s " not_defined ^ commas_quote not_defined) fun check_sorts ((fname, fT), _) = - Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) + Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS) orelse error (cat_lines ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Sat Apr 16 16:15:37 2011 +0200 @@ -65,7 +65,7 @@ fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = - ClauseContext { ctxt = ProofContext.transfer thy ctxt, + ClauseContext { ctxt = Proof_Context.transfer thy ctxt, qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } @@ -145,7 +145,7 @@ val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs - val thy = ProofContext.theory_of ctxt' + val thy = Proof_Context.theory_of ctxt' fun inst t = subst_bounds (rev qs, t) val gs = map inst pre_gs @@ -183,7 +183,7 @@ val Globals {h, ...} = globals val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata - val cert = Thm.cterm_of (ProofContext.theory_of ctxt) + val cert = Thm.cterm_of (Proof_Context.theory_of ctxt) (* Instantiate the GIntro thm with "f" and import into the clause context. *) val lGI = GIntro_thm @@ -203,7 +203,7 @@ HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |> fold_rev (Logic.all o Free) rcfix - |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] + |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] [] |> abstract_over_list (rev qs) in RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} @@ -386,7 +386,7 @@ fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def = let val Globals {h, domT, ranT, x, ...} = globals - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) val ihyp = Term.all domT $ Abs ("z", domT, @@ -447,7 +447,7 @@ [] (* no special monos *) ||> Local_Theory.restore_naming lthy - val cert = cterm_of (ProofContext.theory_of lthy) + val cert = cterm_of (Proof_Context.theory_of lthy) fun requantify orig_intro thm = let val (qs, t) = dest_all_all orig_intro @@ -692,7 +692,7 @@ (* FIXME: broken by design *) fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, qglr = (oqs, _, _, _), ...} = clause val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) @@ -849,8 +849,8 @@ val ((f, (_, f_defthm)), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy - val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss - val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees + val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss + val trees = map (Function_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees val ((R, RIntro_thmss, R_elim), lthy) = PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy @@ -858,10 +858,10 @@ val (_, lthy) = Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy - val newthy = ProofContext.theory_of lthy + val newthy = Proof_Context.theory_of lthy val clauses = map (transfer_clause_ctx newthy) clauses - val cert = cterm_of (ProofContext.theory_of lthy) + val cert = cterm_of (Proof_Context.theory_of lthy) val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/induction_schema.ML Sat Apr 16 16:15:37 2011 +0200 @@ -124,7 +124,7 @@ val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) - val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs + val Cs' = map (Pattern.rewrite_term (Proof_Context.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = HOLogic.mk_Trueprop Pbool @@ -211,7 +211,7 @@ SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val cert = cterm_of thy val P_comp = mk_ind_goal thy branches @@ -351,7 +351,7 @@ val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' val R = Free (Rn, mk_relT ST) val x = Free (xn, ST) - val cert = cterm_of (ProofContext.theory_of ctxt) + val cert = cterm_of (Proof_Context.theory_of ctxt) val ineqss = mk_ineqs R scheme |> map (map (pairself (Thm.assume o cert))) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Sat Apr 16 16:15:37 2011 +0200 @@ -181,7 +181,7 @@ fun lex_order_tac quiet ctxt solve_tac (st: thm) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ((_ $ (_ $ rel)) :: tl) = prems_of st val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel)) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/measure_functions.ML --- a/src/HOL/Tools/Function/measure_functions.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/measure_functions.ML Sat Apr 16 16:15:37 2011 +0200 @@ -29,7 +29,7 @@ fun find_measures ctxt T = DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1) (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT))) - |> cterm_of (ProofContext.theory_of ctxt) |> Goal.init) + |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init) |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) |> Seq.list_of diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Sat Apr 16 16:15:37 2011 +0200 @@ -151,7 +151,7 @@ fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val oqnames = map fst pre_qs val (qs, _) = Variable.variant_fixes oqnames ctxt @@ -198,7 +198,7 @@ fun mk_applied_form ctxt caTs thm = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) in fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm @@ -209,7 +209,7 @@ fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) = let - val cert = cterm_of (ProofContext.theory_of lthy) + val cert = cterm_of (Proof_Context.theory_of lthy) val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => Free (Pname, cargTs ---> HOLogic.boolT)) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Sat Apr 16 16:15:37 2011 +0200 @@ -83,7 +83,7 @@ val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context=ctxt, ...} => SUBGOAL (fn (t, i) => case t of _ $ (_ $ Abs (_, _, body)) => - (case dest_case (ProofContext.theory_of ctxt) body of + (case dest_case (Proof_Context.theory_of ctxt) body of NONE => no_tac | SOME (arg, conv) => let open Conv in @@ -122,7 +122,7 @@ application type correct*) fun apply_inst ctxt t u = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val T = domain_type (fastype_of t); val T' = fastype_of u; val subst = Type.typ_match (Sign.tsig_of thy) (T, T') Vartab.empty @@ -170,7 +170,7 @@ val ((f_binding, fT), mixfix) = the_single fixes; val fname = Binding.name_of f_binding; - val cert = cterm_of (ProofContext.theory_of lthy); + val cert = cterm_of (Proof_Context.theory_of lthy); val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop plain_eqn); val (head, args) = strip_comb lhs; val F = fold_rev lambda (head :: args) rhs; diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/pat_completeness.ML --- a/src/HOL/Tools/Function/pat_completeness.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/pat_completeness.ML Sat Apr 16 16:15:37 2011 +0200 @@ -128,7 +128,7 @@ fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val (vs, subgf) = dest_all_all subgoal val (cases, _ $ thesis) = Logic.strip_horn subgf handle Bind => raise COMPLETENESS diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/pattern_split.ML --- a/src/HOL/Tools/Function/pattern_split.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/pattern_split.ML Sat Apr 16 16:15:37 2011 +0200 @@ -57,7 +57,7 @@ map (fn (vs, subst) => (vs, (v,t)::subst)) substs end in - maps foo (inst_constrs_of (ProofContext.theory_of ctx) T) + maps foo (inst_constrs_of (Proof_Context.theory_of ctx) T) end | pattern_subtract_subst_aux vs t t' = let @@ -76,7 +76,7 @@ (* p - q *) fun pattern_subtract ctx eq2 eq1 = let - val thy = ProofContext.theory_of ctx + val thy = Proof_Context.theory_of ctx val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1 val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2 diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/relation.ML --- a/src/HOL/Tools/Function/relation.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/relation.ML Sat Apr 16 16:15:37 2011 +0200 @@ -33,7 +33,7 @@ case Term.add_vars (prop_of st) [] of [v as (_, T)] => let - val cert = Thm.cterm_of (ProofContext.theory_of ctxt); + val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); val rel' = singleton (Variable.polymorphic ctxt) rel |> map_types Type_Infer.paramify_vars |> Type.constraint T diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sat Apr 16 16:15:37 2011 +0200 @@ -155,7 +155,7 @@ fun reconstruct_tac ctxt D cs (GP (_, gs)) certificate = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val Multiset { msetT, mk_mset, mset_regroup_conv, mset_pwleq_tac, set_of_simps, @@ -300,7 +300,7 @@ fun single_scnp_tac use_tags orders ctxt D = Termination.CALLS (fn (cs, i) => let - val ms_configured = is_some (Multiset_Setup.get (ProofContext.theory_of ctxt)) + val ms_configured = is_some (Multiset_Setup.get (Proof_Context.theory_of ctxt)) val orders' = if ms_configured then orders else filter_out (curry op = MS) orders val gp = gen_probl D cs diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/size.ML Sat Apr 16 16:15:37 2011 +0200 @@ -133,8 +133,8 @@ 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_global (ProofContext.theory_of lthy'); - val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm; + val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy'); + val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm; in (thm', lthy') end; val ((size_def_thms, size_def_thms'), thy') = @@ -152,7 +152,7 @@ ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) ||> Local_Theory.exit_global; - val ctxt = ProofContext.init_global thy'; + val ctxt = Proof_Context.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 da8817d01e7c -r 23f352990944 src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Function/termination.ML Sat Apr 16 16:15:37 2011 +0200 @@ -197,7 +197,7 @@ fun create ctxt chain_tac descent_tac T rel = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val sk = mk_sum_skel rel val Ts = node_types sk T val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts) @@ -272,7 +272,7 @@ fun wf_union_tac ctxt st = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val cert = cterm_of (theory_of_thm st) val ((_ $ (_ $ rel)) :: ineqs) = prems_of st diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Sat Apr 16 16:15:37 2011 +0200 @@ -335,7 +335,7 @@ in fun freeze_spec th ctxt = let - val cert = Thm.cterm_of (ProofContext.theory_of ctxt); + val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt; val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec; in (th RS spec', ctxt') end @@ -600,7 +600,7 @@ in aux o make_nnf ctxt end fun skolemize ctxt = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in skolemize_with_choice_theorems ctxt (choice_theorems thy) end diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Apr 16 16:15:37 2011 +0200 @@ -313,7 +313,7 @@ (* Converts an Isabelle theorem into NNF. *) fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val th = th |> transform_elim_theorem |> zero_var_indexes @@ -376,7 +376,7 @@ (* Convert a theorem to CNF, with additional premises due to skolemization. *) fun cnf_axiom ctxt0 new_skolemizer ax_no th = let - val thy = ProofContext.theory_of ctxt0 + val thy = Proof_Context.theory_of ctxt0 val choice_ths = choice_theorems thy val (opt, (nnf_th, ctxt)) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0 diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Apr 16 16:15:37 2011 +0200 @@ -63,7 +63,7 @@ end; fun infer_types ctxt = - Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); + Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt); (*We use 1 rather than 0 because variable references in clauses may otherwise conflict with variable constraints in the goal...at least, type inference often fails otherwise. @@ -96,7 +96,7 @@ (*Maps metis terms to isabelle terms*) fun hol_term_from_metis_PT ctxt fol_tm = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^ Metis_Term.toString fol_tm) fun tm_to_tt (Metis_Term.Var v) = @@ -260,7 +260,7 @@ fun assume_inf ctxt mode skolem_params atm = inst_excluded_middle - (ProofContext.theory_of ctxt) + (Proof_Context.theory_of ctxt) (singleton (hol_terms_from_metis ctxt mode skolem_params) (Metis_Term.Fn atm)) @@ -270,7 +270,7 @@ can be inferred from terms. *) fun inst_inf ctxt mode old_skolems thpairs fsubst th = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt val i_th = lookth thpairs th val i_th_vars = Term.add_vars (prop_of i_th) [] fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) @@ -396,7 +396,7 @@ fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) val _ = trace_msg ctxt (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) @@ -437,7 +437,7 @@ val refl_idx = 1 + Thm.maxidx_of REFL_THM; fun refl_inf ctxt mode skolem_params t = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt val i_t = singleton (hol_terms_from_metis ctxt mode skolem_params) t val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) val c_t = cterm_incr_types thy refl_idx i_t @@ -455,7 +455,7 @@ | get_ty_arg_size _ _ = 0; fun equality_inf ctxt mode skolem_params (pos, atm) fp fr = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt val m_tm = Metis_Term.Fn atm val [i_atm,i_tm] = hol_terms_from_metis ctxt mode skolem_params [m_tm, fr] val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) @@ -783,7 +783,7 @@ prems_imp_false else let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun match_term p = let val (tyenv, tenv) = diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Sat Apr 16 16:15:37 2011 +0200 @@ -55,7 +55,7 @@ (* Main function to start Metis proof and reconstruction *) fun FOL_SOLVE mode ctxt cls ths0 = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt val type_lits = Config.get ctxt type_lits val new_skolemizer = Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Sat Apr 16 16:15:37 2011 +0200 @@ -650,7 +650,7 @@ fun hol_thm_to_fol is_conjecture ctxt type_lits mode j old_skolems th = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val (old_skolems, (mlits, types_sorts)) = th |> prop_of |> Logic.strip_imp_concl |> conceal_old_skolem_terms j old_skolems @@ -766,7 +766,7 @@ (* Function to generate metis clauses, including comb and type clauses *) fun prepare_metis_problem mode0 ctxt type_lits cls thss = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt (*The modes FO and FT are sticky. HO can be downgraded to FO.*) fun set_mode FO = FO | set_mode HO = diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 16 16:15:37 2011 +0200 @@ -437,7 +437,7 @@ exists (exists (curry (op =) name o shortest_name o fst) o datatype_constrs hol_ctxt) deep_dataTs val likely_in_struct_induct_step = - exists is_struct_induct_step (ProofContext.cases_of ctxt) + exists is_struct_induct_step (Proof_Context.cases_of ctxt) val _ = if standard andalso likely_in_struct_induct_step then pprint_m (fn () => Pretty.blk (0, pstrs "Hint: To check that the induction hypothesis is \ diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 16 16:15:37 2011 +0200 @@ -577,7 +577,7 @@ handle Type.TYPE_MATCH => raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) fun varify_and_instantiate_type ctxt T1 T1' T2 = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) end @@ -639,11 +639,11 @@ is_some (Quotient_Info.quotdata_lookup_raw thy s) | is_real_quot_type _ _ = false fun is_quot_type ctxt T = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in is_real_quot_type thy T andalso not (is_codatatype ctxt T) end fun is_pure_typedef ctxt (T as Type (s, _)) = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in is_typedef ctxt s andalso not (is_real_datatype thy s orelse is_real_quot_type thy T orelse is_codatatype ctxt T orelse is_record_type T orelse @@ -674,7 +674,7 @@ | NONE => false) | is_univ_typedef _ _ = false fun is_datatype ctxt stds (T as Type (s, _)) = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in (is_typedef ctxt s orelse is_codatatype ctxt T orelse T = @{typ ind} orelse is_real_quot_type thy T) andalso not (is_basic_datatype thy stds s) @@ -765,7 +765,7 @@ @{const_name Quot}, @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val (x as (_, T)) = (s, unarize_unbox_etc_type T) in is_real_constr thy x orelse is_record_constr x orelse @@ -776,7 +776,7 @@ is_codatatype ctxt (body_type T) andalso is_constr_like ctxt x andalso not (is_coconstr ctxt x) fun is_constr ctxt stds (x as (_, T)) = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in is_constr_like ctxt x andalso not (is_basic_datatype thy stds (fst (dest_Type (unarize_type (body_type T))))) andalso @@ -1135,7 +1135,7 @@ in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end end fun select_nth_constr_arg ctxt stds x t n res_T = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in (case strip_comb t of (Const x', args) => if x = x' then nth args n @@ -1300,7 +1300,7 @@ fun all_axioms_of ctxt subst = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val axioms_of_thys = maps Thm.axioms_of #> map (apsnd (subst_atomic subst o prop_of)) @@ -1441,7 +1441,7 @@ | t => t) fun case_const_names ctxt stds = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) => if is_basic_datatype thy stds dtype_s then I @@ -1889,7 +1889,7 @@ |> const_nondef_table fun inductive_intro_table ctxt subst def_tables = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in def_table_for (maps (map (unfold_mutually_inductive_preds thy def_tables o prop_of) o snd o snd) @@ -1922,7 +1922,7 @@ fun inverse_axioms_for_rep_fun ctxt (x as (_, T)) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val abs_T = domain_type T in typedef_info ctxt (fst (dest_Type abs_T)) |> the @@ -1932,7 +1932,7 @@ end fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val abs_T = Type abs_z in if is_univ_typedef ctxt abs_T then @@ -1957,7 +1957,7 @@ end fun optimized_quot_type_axioms ctxt stds abs_z = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val abs_T = Type abs_z val rep_T = rep_type_for_quot_type thy abs_T val (equiv_rel, partial) = equiv_relation_for_quot_type thy abs_T diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 16 16:15:37 2011 +0200 @@ -303,7 +303,7 @@ end fun default_params thy = - extract_params (ProofContext.init_global thy) false (default_raw_params thy) + extract_params (Proof_Context.init_global thy) false (default_raw_params thy) o map (apsnd single) val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 16 16:15:37 2011 +0200 @@ -94,7 +94,7 @@ fun add_wacky_syntax ctxt = let val name_of = fst o dest_Const - val thy = ProofContext.theory_of ctxt |> Context.reject_draft + val thy = Proof_Context.theory_of ctxt |> Context.reject_draft val (maybe_t, thy) = Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}), Mixfix (maybe_mixfix (), [1000], 1000)) thy @@ -109,7 +109,7 @@ Mixfix (step_mixfix (), [1000], 1000)) thy in (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)), - ProofContext.transfer_syntax thy ctxt) + Proof_Context.transfer_syntax thy ctxt) end (** Term reconstruction **) @@ -329,7 +329,7 @@ | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], []) fun varified_type_match ctxt (candid_T, pat_T) = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in strict_type_match thy (candid_T, varify_type ctxt pat_T) end diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 16 16:15:37 2011 +0200 @@ -69,7 +69,7 @@ fun add_to_uncurry_table ctxt t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun aux (t1 $ t2) args table = let val table = aux t2 [] table in aux t1 (t2 :: args) table end | aux (Abs (_, _, t')) _ table = aux t' [] table diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Apr 16 16:15:37 2011 +0200 @@ -312,7 +312,7 @@ fun translate_intros ensure_groundness ctxt gr const constant_table = let - val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const) + val intros = map (preprocess_intro (Proof_Context.theory_of ctxt)) (Graph.get_node gr const) val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table fun translate_intro intro = @@ -550,7 +550,7 @@ in (clause :: flat rec_clauses, (seen', constant_table'')) end - val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T + val constrs = inst_constrs_of (Proof_Context.theory_of ctxt) T val constrs' = (constrs ~~ map (is_recursive_constr T) constrs) |> (fn cs => filter_out snd cs @ filter snd cs) val (clauses, constant_table') = @@ -873,7 +873,7 @@ | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T) | restore_term ctxt constant_table (AppF (f, args), T) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val c = restore_const constant_table f val cT = Sign.the_const_type thy c val (argsT, resT) = strip_type cT @@ -923,7 +923,7 @@ fun values ctxt soln t_compr = let - val options = code_options_of (ProofContext.theory_of ctxt) + val options = code_options_of (Proof_Context.theory_of ctxt) val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr); val (body, Ts, fp) = HOLogic.strip_psplits split; @@ -936,12 +936,12 @@ (Const (name, T), all_args) => (Const (name, T), all_args) | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head) val _ = tracing "Preprocessing specification..." - val T = Sign.the_const_type (ProofContext.theory_of ctxt) name + val T = Sign.the_const_type (Proof_Context.theory_of ctxt) name val t = Const (name, T) val thy' = - Theory.copy (ProofContext.theory_of ctxt) + Theory.copy (Proof_Context.theory_of ctxt) |> Predicate_Compile.preprocess preprocess_options t - val ctxt' = ProofContext.init_global thy' + val ctxt' = Proof_Context.init_global thy' val _ = tracing "Generating prolog program..." val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *) |> post_process ctxt' options name @@ -1012,13 +1012,13 @@ fun quickcheck ctxt [(t, [])] [_, size] = let val t' = list_abs_free (Term.add_frees t [], t) - val options = code_options_of (ProofContext.theory_of ctxt) - val thy = Theory.copy (ProofContext.theory_of ctxt) + val options = code_options_of (Proof_Context.theory_of ctxt) + val thy = Theory.copy (Proof_Context.theory_of ctxt) val ((((full_constname, constT), vs'), intro), thy1) = Predicate_Compile_Aux.define_quickcheck_predicate t' thy val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2 - val ctxt' = ProofContext.init_global thy3 + val ctxt' = Proof_Context.init_global thy3 val _ = tracing "Generating prolog program..." val (p, constant_table) = generate (NONE, true) ctxt' full_constname |> post_process ctxt' (set_ensure_groundness options) full_constname diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Sat Apr 16 16:15:37 2011 +0200 @@ -136,7 +136,7 @@ (* queries *) fun lookup_pred_data ctxt name = - Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name) + Option.map rep_pred_data (try (Graph.get_node (PredData.get (Proof_Context.theory_of ctxt))) name) fun the_pred_data ctxt name = case lookup_pred_data ctxt name of NONE => error ("No such predicate " ^ quote name) @@ -144,7 +144,7 @@ val is_registered = is_some oo lookup_pred_data -val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of +val all_preds_of = Graph.keys o PredData.get o Proof_Context.theory_of val intros_of = map snd o #intros oo the_pred_data @@ -203,11 +203,11 @@ val predfun_neg_intro_of = #neg_intro ooo the_predfun_data val intros_graph_of = - Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of + Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o Proof_Context.theory_of fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val nargs = length (binder_types (fastype_of pred)) fun PEEK f dependent_tactic st = dependent_tactic (f st) st fun meta_eq_of th = th RS @{thm eq_reflection} @@ -257,7 +257,7 @@ let val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) in (fst (dest_Const const) = name) end; - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result)) val index = find_index (fn s => s = name) (#names (fst info)) val pre_elim = nth (#elims result) index @@ -330,7 +330,7 @@ val pred = Const (constname, T) val pre_elim = (Drule.export_without_context o Skip_Proof.make_thm thy) - (mk_casesrule (ProofContext.init_global thy) pred pre_intros) + (mk_casesrule (Proof_Context.init_global thy) pred pre_intros) in register_predicate (constname, pre_intros, pre_elim) thy end fun defined_function_of compilation pred = @@ -371,7 +371,7 @@ fun extend_intro_graph names thy = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy in PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names) thy end @@ -384,7 +384,7 @@ val (named_intros, SOME elim) = rules val named_intros' = map (apsnd (preprocess_intro thy)) named_intros val pred = Const (name, Sign.the_const_type thy name) - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy val elim_t = mk_casesrule ctxt pred (map snd named_intros') val nparams = (case try (Inductive.the_inductive ctxt) name of SOME (_, result) => length (Inductive.params_of (#raw_induct result)) @@ -410,7 +410,7 @@ fun alternative_compilation_of ctxt pred_name mode = AList.lookup eq_mode - (Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode + (Symtab.lookup_list (Alt_Compilations_Data.get (Proof_Context.theory_of ctxt)) pred_name) mode fun force_modes_and_compilations pred_name compilations = let diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Apr 16 16:15:37 2011 +0200 @@ -76,7 +76,7 @@ fun preprocess_strong_conn_constnames options gr ts thy = if forall (fn (Const (c, _)) => - Core_Data.is_registered (ProofContext.init_global thy) c) ts then + Core_Data.is_registered (Proof_Context.init_global thy) c) ts then thy else let @@ -149,7 +149,7 @@ val proposed_modes = case proposed_modes of Single_Pred proposed_modes => [(const, proposed_modes)] | Multiple_Preds proposed_modes => map - (apfst (Code.read_const (ProofContext.theory_of lthy))) proposed_modes + (apfst (Code.read_const (Proof_Context.theory_of lthy))) proposed_modes in Options { expected_modes = Option.map (pair const) expected_modes, @@ -181,7 +181,7 @@ fun code_pred_cmd (((expected_modes, proposed_modes), raw_options), raw_const) lthy = let - val thy = ProofContext.theory_of lthy + val thy = Proof_Context.theory_of lthy val const = Code.read_const thy raw_const val T = Sign.the_const_type thy const val t = Const (const, T) @@ -191,7 +191,7 @@ let val lthy' = Local_Theory.background_theory (preprocess options t) lthy val const = - case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of + case Predicate_Compile_Fun.pred_of_function (Proof_Context.theory_of lthy') const of SOME c => c | NONE => const val _ = print_step options "Starting Predicate Compile Core..." diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Apr 16 16:15:37 2011 +0200 @@ -530,7 +530,7 @@ else false *) -val is_constr = Code.is_constr o ProofContext.theory_of; +val is_constr = Code.is_constr o Proof_Context.theory_of; fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t) @@ -830,7 +830,7 @@ (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t @@ -873,7 +873,7 @@ fun expand_tuples thy intro = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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 @@ -942,7 +942,7 @@ fun instantiated_case_rewrites thy Tcon = let val rew_ths = case_rewrites thy Tcon - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy fun instantiate th = let val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))) @@ -1045,7 +1045,7 @@ fun peephole_optimisation thy intro = let val process = - Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy)) + Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.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 = @@ -1072,7 +1072,7 @@ | import_intros inp_pred (th :: ths) ctxt = let val ((_, [th']), ctxt') = Variable.import true [th] ctxt - val thy = ProofContext.theory_of ctxt' + val thy = Proof_Context.theory_of ctxt' val (pred, args) = strip_intro_concl th' val T = fastype_of pred val ho_args = ho_args_of_typ T args @@ -1206,7 +1206,7 @@ fun define_quickcheck_predicate t thy = let val (vs, t') = strip_abs t - val vs' = Variable.variant_frees (ProofContext.init_global thy) [] vs + val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs val t'' = subst_bounds (map Free (rev vs'), t') val (prems, concl) = strip_horn t'' val constname = "quickcheck" @@ -1218,7 +1218,7 @@ (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), HOLogic.mk_Trueprop (list_comb (const, map Free vs'))) val tac = fn _ => Skip_Proof.cheat_tac thy1 - val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac + val intro = Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t tac in ((((full_constname, constT), vs'), intro), thy1) end diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Apr 16 16:15:37 2011 +0200 @@ -128,7 +128,7 @@ fun print_stored_rules ctxt = let - val preds = Graph.keys (PredData.get (ProofContext.theory_of ctxt)) + val preds = Graph.keys (PredData.get (Proof_Context.theory_of ctxt)) fun print pred () = let val _ = writeln ("predicate: " ^ pred) val _ = writeln ("introrules: ") @@ -818,7 +818,7 @@ case T of TFree _ => NONE | Type (Tcon, _) => - (case Datatype_Data.get_constrs (ProofContext.theory_of ctxt) Tcon of + (case Datatype_Data.get_constrs (Proof_Context.theory_of ctxt) Tcon of NONE => NONE | SOME cs => (case strip_comb t of @@ -881,7 +881,7 @@ in_ts' outTs switch_tree = let val compfuns = Comp_Mod.compfuns compilation_modifiers - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun compile_switch_tree _ _ (Atom []) = NONE | compile_switch_tree all_vs ctxt_eqs (Atom moded_clauses) = let @@ -1125,7 +1125,7 @@ val ([definition], thy') = thy |> Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |> Global_Theory.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])] - val ctxt' = ProofContext.init_global thy' + val ctxt' = Proof_Context.init_global thy' val rules as ((intro, elim), _) = create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T)) in thy' @@ -1202,7 +1202,7 @@ fun prepare_intrs options ctxt prednames intros = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val intrs = map prop_of intros val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames val (preds, intrs) = unify_consts thy preds intrs @@ -1289,7 +1289,7 @@ val nparams = nparams_of thy predname val elim' = (Drule.export_without_context o Skip_Proof.make_thm thy) - (mk_casesrule (ProofContext.init_global thy) nparams intros) + (mk_casesrule (Proof_Context.init_global thy) nparams intros) in if not (Thm.equiv_thm (elim, elim')) then error "Introduction and elimination rules do not match!" @@ -1349,7 +1349,7 @@ let fun dest_steps (Steps s) = s val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps)) - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy val _ = print_step options ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation ^ ") for predicates " ^ commas prednames ^ "...") @@ -1378,7 +1378,7 @@ cond_timeit (Config.get ctxt Quickcheck.timing) "Defining executable functions..." (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy' |> Theory.checkpoint) - val ctxt'' = ProofContext.init_global thy'' + val ctxt'' = Proof_Context.init_global thy'' val _ = print_step options "Compiling equations..." val compiled_terms = cond_timeit (Config.get ctxt Quickcheck.timing) "Compiling equations...." (fn _ => @@ -1415,7 +1415,7 @@ val thy'' = fold preprocess_intros (flat scc) thy' val thy''' = fold_rev (fn preds => fn thy => - if not (forall (defined (ProofContext.init_global thy)) preds) then + if not (forall (defined (Proof_Context.init_global thy)) preds) then let val mode_analysis_options = {use_generators = #use_generators (dest_steps steps), reorder_premises = @@ -1581,11 +1581,11 @@ (* FIXME ... this is important to avoid changing the background theory below *) fun generic_code_pred prep_const options raw_const lthy = let - val thy = ProofContext.theory_of lthy + val thy = Proof_Context.theory_of lthy val const = prep_const thy raw_const val lthy' = Local_Theory.background_theory (extend_intro_graph [const]) lthy - val thy' = ProofContext.theory_of lthy' - val ctxt' = ProofContext.init_global thy' + val thy' = Proof_Context.theory_of lthy' + val ctxt' = Proof_Context.init_global thy' val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt') fun mk_cases const = let @@ -1603,11 +1603,11 @@ val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases val lthy'' = lthy' |> fold Variable.auto_fixes cases_rules - |> ProofContext.add_cases true case_env + |> Proof_Context.add_cases true case_env fun after_qed thms goal_ctxt = let - val global_thms = ProofContext.export goal_ctxt - (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms) + val global_thms = Proof_Context.export goal_ctxt + (Proof_Context.init_global (Proof_Context.theory_of goal_ctxt)) (map the_single thms) in goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #> ((case compilation options of @@ -1834,7 +1834,7 @@ @{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t else mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val time_limit = seconds (Config.get ctxt values_timeout) val (ts, statistics) = (case compilation of diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Apr 16 16:15:37 2011 +0200 @@ -134,7 +134,7 @@ fun split_all_pairs thy th = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy val ((_, [th']), ctxt') = Variable.import true [th] ctxt val t = prop_of th' val frees = Term.add_frees t [] @@ -158,7 +158,7 @@ fun inline_equations thy th = let - val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init_global thy) + val inline_defs = Predicate_Compile_Inline_Defs.get (Proof_Context.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)) @@ -193,7 +193,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_global thy + val ctxt = Proof_Context.init_global thy fun filtering th = if is_equationlike th andalso defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then @@ -259,7 +259,7 @@ fun obtain_specification_graph options thy t = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy fun is_nondefining_const (c, T) = member (op =) logic_operator_names c fun has_code_pred_intros (c, T) = can (Core_Data.intros_of ctxt) c fun case_consts (c, T) = is_some (Datatype.info_of_case thy c) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sat Apr 16 16:15:37 2011 +0200 @@ -183,7 +183,7 @@ SOME raw_split_thm => let val (f, args) = strip_comb t - val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm + val split_thm = prepare_split_thm (Proof_Context.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 t' = case_betapply thy t diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sat Apr 16 16:15:37 2011 +0200 @@ -32,10 +32,10 @@ NONE => NONE | SOME raw_split_thm => let - val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm + val split_thm = prepare_split_thm (Proof_Context.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_global thy)*) + Variable.import true [split_thm] (Proof_Context.init_global thy)*) val (assms, concl) = Logic.strip_horn (prop_of split_thm) val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) val atom' = case_betapply thy atom @@ -127,11 +127,11 @@ fun flatten_intros constname intros thy = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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) - val ctxt'' = ProofContext.transfer thy' ctxt' + val ctxt'' = Proof_Context.transfer thy' ctxt' val tac = fn _ => Skip_Proof.cheat_tac thy' val intros'' = map (fn t => Goal.prove ctxt'' [] [] t tac) intros' |> Variable.export ctxt'' ctxt @@ -146,7 +146,7 @@ fun introrulify thy ths = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy val ((_, ths'), ctxt') = Variable.import true ths ctxt fun introrulify' th = let @@ -189,7 +189,7 @@ Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}]) #> Simplifier.full_simplify (HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps}) - #> split_conjuncts_in_assms (ProofContext.init_global thy) + #> split_conjuncts_in_assms (Proof_Context.init_global thy) fun print_specs options thy msg ths = if show_intermediate_results options then @@ -202,7 +202,7 @@ SOME specss => (specss, thy) | NONE =>*) let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.init_global thy val intros = if forall is_pred_equation specs then map (split_conjuncts_in_assms ctxt) (introrulify thy (map rewrite specs)) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sat Apr 16 16:15:37 2011 +0200 @@ -157,7 +157,7 @@ fun prove_match options ctxt nargs out_ts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val eval_if_P = @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} fun get_case_rewrite t = @@ -324,7 +324,7 @@ fun prove_match2 options ctxt out_ts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun split_term_tac (Free _) = all_tac | split_term_tac t = if (is_constructor thy t) then @@ -507,7 +507,7 @@ fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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 diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sat Apr 16 16:15:37 2011 +0200 @@ -218,7 +218,7 @@ fun compile_term compilation options ctxt [(t, eval_terms)] = let val t' = list_abs_free (Term.add_frees t [], t) - val thy = Theory.copy (ProofContext.theory_of ctxt) + val thy = Theory.copy (Proof_Context.theory_of ctxt) val ((((full_constname, constT), vs'), intro), thy1) = Predicate_Compile_Aux.define_quickcheck_predicate t' thy val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 @@ -238,7 +238,7 @@ (*val _ = Predicate_Compile_Core.print_all_modes compilation thy4*) val _ = Output.tracing ("Preprocessing time: " ^ string_of_int (snd preproc_time)) val _ = Output.tracing ("Core compilation time: " ^ string_of_int (snd core_comp_time)) - val ctxt4 = ProofContext.init_global thy4 + val ctxt4 = Proof_Context.init_global thy4 val modes = Core_Data.modes_of compilation ctxt4 full_constname val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool val prog = diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Sat Apr 16 16:15:37 2011 +0200 @@ -33,7 +33,7 @@ fun import (pred, intros) args ctxt = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ((Tinst, intros'), ctxt') = Variable.importT intros ctxt val pred' = fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros'))))) val Ts = binder_types (fastype_of pred') @@ -64,7 +64,7 @@ fun specialise_intros black_list (pred, intros) pats thy = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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 @@ -180,7 +180,7 @@ if member (op =) ((map fst specs) @ black_list) pred_name then thy else - (case try (Core_Data.intros_of (ProofContext.init_global thy)) pred_name of + (case try (Core_Data.intros_of (Proof_Context.init_global thy)) pred_name of NONE => thy | SOME [] => thy | SOME intros => diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Sat Apr 16 16:15:37 2011 +0200 @@ -682,7 +682,7 @@ val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (@{binding cooper}, (fn (ctxt, t) => - (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop) + (Thm.cterm_of (Proof_Context.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop) (t, procedure t))))); val comp_ss = HOL_ss addsimps @{thms semiring_norm}; diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Apr 16 16:15:37 2011 +0200 @@ -289,7 +289,7 @@ fun mk_fast_generator_expr ctxt (t, eval_terms) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ctxt' = Variable.auto_fixes t ctxt val names = Term.add_free_names t [] val frees = map Free (Term.add_frees t []) @@ -329,7 +329,7 @@ fun mk_generator_expr ctxt (t, eval_terms) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ctxt' = Variable.auto_fixes t ctxt val names = Term.add_free_names t [] val frees = map Free (Term.add_frees t []) @@ -371,7 +371,7 @@ fun mk_full_generator_expr ctxt (t, eval_terms) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ctxt' = Variable.auto_fixes t ctxt val names = Term.add_free_names t [] val frees = map Free (Term.add_frees t []) @@ -428,7 +428,7 @@ fun mk_validator_expr ctxt t = let fun bounded_forallT T = (T --> @{typ bool}) --> @{typ code_numeral} --> @{typ bool} - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ctxt' = Variable.auto_fixes t ctxt val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt' val depth = Free (depth_name, @{typ code_numeral}) @@ -490,7 +490,7 @@ fun compile_generator_expr ctxt ts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val mk_generator_expr = if Config.get ctxt fast then mk_fast_generator_expr else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr @@ -507,7 +507,7 @@ fun compile_generator_exprs ctxt ts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts; val compiles = Code_Runtime.dynamic_value_strict (Counterexample_Batch.get, put_counterexample_batch, @@ -521,7 +521,7 @@ fun compile_validator_exprs ctxt ts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ts' = map (mk_validator_expr ctxt) ts in Code_Runtime.dynamic_value_strict diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Apr 16 16:15:37 2011 +0200 @@ -141,7 +141,7 @@ fun evaluation cookie thy evaluator vs_t args size = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; val (program_code, value_name) = evaluator vs_t; val value_code = space_implode " " (value_name :: "()" :: map (enclose "(" ")") args); @@ -192,7 +192,7 @@ fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val t' = list_abs_free (Term.add_frees t [], t) val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t' fun ensure_testable t = diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Apr 16 16:15:37 2011 +0200 @@ -65,7 +65,7 @@ let val eqs_t = mk_equations consts val eqs = map (fn eq => Goal.prove lthy argnames [] eq - (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t + (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t in fold (fn (name, eq) => Local_Theory.note ((Binding.conceal (Binding.qualify true prfx diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sat Apr 16 16:15:37 2011 +0200 @@ -83,7 +83,7 @@ fun random_aux_primrec eq lthy = let - val thy = ProofContext.theory_of lthy; + val thy = Proof_Context.theory_of lthy; val ((t_random_aux as Free (random_aux, T)) $ (t_k as Free (v, _)), proto_t_rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; val Type (_, [_, iT]) = T; @@ -104,7 +104,7 @@ [(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)]); val tac = ALLGOALS (rtac rule) THEN ALLGOALS (simp_tac rew_ss) - THEN (ALLGOALS (ProofContext.fact_tac eqs2)) + THEN (ALLGOALS (Proof_Context.fact_tac eqs2)) val simp = Skip_Proof.prove lthy' [v] [] eq (K tac); in (simp, lthy') end; @@ -116,7 +116,7 @@ |>> (fn simp => [simp]) | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy = let - val thy = ProofContext.theory_of lthy; + val thy = Proof_Context.theory_of lthy; val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs; val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss; val Ts = map fastype_of lhss; @@ -162,7 +162,7 @@ fun prove_simps proto_simps lthy = let val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps; - val tac = ALLGOALS (ProofContext.fact_tac ext_simps); + val tac = ALLGOALS (Proof_Context.fact_tac ext_simps); in (map (fn prop => Skip_Proof.prove lthy vs [] prop (K tac)) eqs, lthy) end; val b = Binding.conceal (Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"))); @@ -290,7 +290,7 @@ fun mk_generator_expr ctxt (t, eval_terms) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val prop = list_abs_free (Term.add_frees t [], t) val Ts = (map snd o fst o strip_abs) prop val bound_max = length Ts - 1; @@ -316,7 +316,7 @@ fun mk_reporting_generator_expr ctxt (t, eval_terms) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val prop = list_abs_free (Term.add_frees t [], t) val Ts = (map snd o fst o strip_abs) prop val bound_max = length Ts - 1 @@ -393,7 +393,7 @@ fun compile_generator_expr ctxt ts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val iterations = Config.get ctxt Quickcheck.iterations in if Config.get ctxt Quickcheck.report then diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Sat Apr 16 16:15:37 2011 +0200 @@ -77,7 +77,7 @@ | NONE => raise NotFound) fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) -fun maps_update k minfo = ProofContext.background_theory (maps_update_thy k minfo) (* FIXME *) +fun maps_update k minfo = Proof_Context.background_theory (maps_update_thy k minfo) (* FIXME *) fun maps_attribute_aux s minfo = Thm.declaration_attribute (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) @@ -85,7 +85,7 @@ (* attribute to be used in declare statements *) fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val tyname = Sign.intern_type thy tystr val mapname = Sign.intern_const thy mapstr val relname = Sign.intern_const thy relstr @@ -111,7 +111,7 @@ "map:", mapfun, "relation map:", relmap])) in - MapsData.get (ProofContext.theory_of ctxt) + MapsData.get (Proof_Context.theory_of ctxt) |> Symtab.dest |> map (prt_map) |> Pretty.big_list "maps for type constructors:" @@ -147,7 +147,7 @@ fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I fun quotdata_dest lthy = - map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy))) + map snd (Symtab.dest (QuotData.get (Proof_Context.theory_of lthy))) fun print_quotinfo ctxt = let @@ -162,7 +162,7 @@ Pretty.str "equiv. thm:", Syntax.pretty_term ctxt (prop_of equiv_thm)]) in - QuotData.get (ProofContext.theory_of ctxt) + QuotData.get (Proof_Context.theory_of ctxt) |> Symtab.dest |> map (prt_quot o snd) |> Pretty.big_list "quotients:" @@ -195,7 +195,7 @@ fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I fun qconsts_dest lthy = - flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy)))) + flat (map snd (Symtab.dest (QConstsData.get (Proof_Context.theory_of lthy)))) fun qconsts_lookup thy t = let @@ -225,7 +225,7 @@ Pretty.str "as", Syntax.pretty_term ctxt (prop_of def)]) in - QConstsData.get (ProofContext.theory_of ctxt) + QConstsData.get (Proof_Context.theory_of ctxt) |> Symtab.dest |> map snd |> flat diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Apr 16 16:15:37 2011 +0200 @@ -98,7 +98,7 @@ *) fun calculate_inst ctxt ball_bex_thm redex R1 R2 = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] val trm_inst = map (SOME o cterm_of thy) [R2, R1] @@ -156,7 +156,7 @@ fun regularize_tac ctxt = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} val simproc = @@ -201,7 +201,7 @@ (Const (@{const_name Quot_True}, _) $ x) => let val fx = fnctn x; - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val cx = cterm_of thy x; val cfx = cterm_of thy fx; val cxt = ctyp_of thy (fastype_of x); @@ -253,7 +253,7 @@ val ty_x = fastype_of x val ty_b = fastype_of qt_arg val ty_f = range_type (fastype_of f) - val thy = ProofContext.theory_of context + val thy = Proof_Context.theory_of context val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; val inst_thm = Drule.instantiate' ty_inst @@ -269,7 +269,7 @@ *) fun equals_rsp_tac R ctxt = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt in case try (cterm_of thy) R of (* There can be loose bounds in R *) SOME ctm => @@ -290,7 +290,7 @@ SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac | SOME (rel $ _ $ (rep $ (abs $ _))) => let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val (ty_a, ty_b) = dest_funT (fastype_of abs); val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; in @@ -478,7 +478,7 @@ (case term_of ctrm of (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val (ty_b, ty_a) = dest_funT (fastype_of r1) val (ty_c, ty_d) = dest_funT (fastype_of a2) val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] @@ -556,7 +556,7 @@ fun gen_frees_tac ctxt = SUBGOAL (fn (concl, i) => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val vrs = Term.add_frees concl [] val cvrs = map (cterm_of thy o Free) vrs val concl' = apply_under_Trueprop (all_list vrs) concl @@ -600,7 +600,7 @@ fun procedure_inst ctxt rtrm qtrm = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val rtrm' = HOLogic.dest_Trueprop rtrm val qtrm' = HOLogic.dest_Trueprop qtrm val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm') @@ -704,7 +704,7 @@ in Goal.prove ctxt' [] [] goal (K (HEADGOAL (lift_single_tac ctxt' simps rthm'))) - |> singleton (ProofContext.export ctxt' ctxt) + |> singleton (Proof_Context.export ctxt' ctxt) end diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Sat Apr 16 16:15:37 2011 +0200 @@ -64,7 +64,7 @@ fun get_mapfun ctxt s = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val mapfun = #mapfun (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") in @@ -101,7 +101,7 @@ *) fun get_rty_qty ctxt s = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") in @@ -122,7 +122,7 @@ (* matches a type pattern with a type *) fun match ctxt err ty_pat ty = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt in Sign.typ_match thy (ty_pat, ty) Vartab.empty handle Type.TYPE_MATCH => err ctxt ty_pat ty @@ -258,7 +258,7 @@ (* instantiates TVars so that the term is of type ty *) fun force_typ ctxt trm ty = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val trm_ty = fastype_of trm val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty in @@ -273,7 +273,7 @@ fun get_relmap ctxt s = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val relmap = #relmap (Quotient_Info.maps_lookup thy s) handle Quotient_Info.NotFound => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") in @@ -296,7 +296,7 @@ fun get_equiv_rel ctxt s = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt in #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") @@ -554,7 +554,7 @@ | (_, Const _) => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T' | same_const _ _ = false in @@ -707,7 +707,7 @@ case rty of Type (s, rtys) => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys) fun matches [] = rty' @@ -729,7 +729,7 @@ | Bound i => Bound i | Const (a, ty) => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun matches [] = Const (a, subst_typ ctxt ty_subst ty) | matches ((rconst, qconst)::tail) = @@ -749,7 +749,7 @@ *) fun mk_ty_subst qtys direction ctxt = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt in Quotient_Info.quotdata_dest ctxt |> map (fn x => (#rtyp x, #qtyp x)) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Sat Apr 16 16:15:37 2011 +0200 @@ -215,7 +215,7 @@ (* check for existence of map functions *) fun map_check ctxt (_, (rty, _, _)) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun map_check_aux rty warns = case rty of diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/SMT/smt_builtin.ML --- a/src/HOL/Tools/SMT/smt_builtin.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_builtin.ML Sat Apr 16 16:15:37 2011 +0200 @@ -73,7 +73,7 @@ SMT_Utils.dict_merge (Ord_List.merge typ_ord) ttabp fun lookup_ttab ctxt ttab T = - let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U) + let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U) in get_first (find_first match) (SMT_Utils.dict_lookup ttab (SMT_Config.solver_class_of ctxt)) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/SMT/smt_datatypes.ML --- a/src/HOL/Tools/SMT/smt_datatypes.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML Sat Apr 16 16:15:37 2011 +0200 @@ -62,7 +62,7 @@ fun get_record_decl ({ext_def, ...} : Record.info) T ctxt = let val (con, _) = Term.dest_Const (lhs_head_of ext_def) - val (fields, more) = Record.get_extT_fields (ProofContext.theory_of ctxt) T + val (fields, more) = Record.get_extT_fields (Proof_Context.theory_of ctxt) T val fieldTs = map snd fields @ [snd more] val constr = Const (con, fieldTs ---> T) @@ -89,7 +89,7 @@ fun declared declss T = exists (exists (equal T o fst)) declss fun get_decls T n Ts ctxt = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt in (case Datatype.get_info thy n of SOME info => get_datatype_decl info n Ts ctxt diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/SMT/smt_monomorph.ML --- a/src/HOL/Tools/SMT/smt_monomorph.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML Sat Apr 16 16:15:37 2011 +0200 @@ -121,7 +121,7 @@ fun search_substitutions ctxt limit instances all_grounds new_grounds scss = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds) val spec = specialize thy limit all_grounds' new_grounds val (scss', (new_grounds', instances')) = @@ -162,7 +162,7 @@ fun instantiate full (i, thm) substs (ithms, ctxt) = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) []) val (Tenv, ctxt') = @@ -215,7 +215,7 @@ in scss |> search_substitutions ctxt limit instances Symtab.empty grounds - |> map (filter_most_specific (ProofContext.theory_of ctxt)) + |> map (filter_most_specific (Proof_Context.theory_of ctxt)) |> rpair (monos, ctxt) |-> fold2 (instantiate full) polys end diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Sat Apr 16 16:15:37 2011 +0200 @@ -170,7 +170,7 @@ (case Term.strip_comb t of (Const c, ts as _ :: _) => not (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso - forall (is_constr_pat (ProofContext.theory_of ctxt)) ts + forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts | _ => false) fun has_all_vars vs t = @@ -218,7 +218,7 @@ val (lhs, rhs) = dest_cond_eq ct val vs = map Thm.term_of cvs - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun get_mpats ct = if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/SMT/smt_utils.ML --- a/src/HOL/Tools/SMT/smt_utils.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_utils.ML Sat Apr 16 16:15:37 2011 +0200 @@ -162,7 +162,7 @@ (* certified terms *) -fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) +fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt) fun typ_of ct = #T (Thm.rep_cterm ct) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/SMT/z3_interface.ML --- a/src/HOL/Tools/SMT/z3_interface.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/SMT/z3_interface.ML Sat Apr 16 16:15:37 2011 +0200 @@ -102,11 +102,11 @@ chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs fun chained_mk_builtin_num ctxt bs i T = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end fun chained_mk_builtin_fun ctxt bs s cts = - let val thy = ProofContext.theory_of ctxt + let val thy = Proof_Context.theory_of ctxt in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat Apr 16 16:15:37 2011 +0200 @@ -833,7 +833,7 @@ fun discharge rules outer_ctxt (p, (inner_ctxt, _)) = thm_of p - |> singleton (ProofContext.export inner_ctxt outer_ctxt) + |> singleton (Proof_Context.export inner_ctxt outer_ctxt) |> discharge_assms (make_discharge_rules rules) in diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sat Apr 16 16:15:37 2011 +0200 @@ -457,7 +457,7 @@ fun check_formula ctxt = Type.constraint HOLogic.boolT - #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) + #> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (**** Translation of TSTP files to Isar Proofs ****) @@ -467,7 +467,7 @@ fun decode_line type_sys tfrees (Definition (name, phi1, phi2)) ctxt = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val t1 = prop_from_formula thy type_sys tfrees phi1 val vars = snd (strip_comb t1) val frees = map unvarify_term vars @@ -483,7 +483,7 @@ end | decode_line type_sys tfrees (Inference (name, u, deps)) ctxt = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val t = u |> prop_from_formula thy type_sys tfrees |> uncombine_term |> check_formula ctxt in diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sat Apr 16 16:15:37 2011 +0200 @@ -188,7 +188,7 @@ in aux (maxidx_of_term t + 1) t end fun introduce_combinators_in_term ctxt kind t = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in if Meson.is_fol_term thy t then t else @@ -241,7 +241,7 @@ (* making fact and conjecture formulas *) fun make_formula ctxt eq_as_iff presimp name kind t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val t = t |> Envir.beta_eta_contract |> transform_elim_term |> Object_Logic.atomize_term thy @@ -324,7 +324,7 @@ fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val fact_ts = map (prop_of o snd o snd) rich_facts val (facts, fact_names) = rich_facts @@ -375,7 +375,7 @@ is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts | is_type_dangerous _ _ = false and is_type_constr_dangerous ctxt s = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in case Datatype_Data.get_info thy s of SOME {descr, ...} => forall (fn (_, (_, _, constrs)) => @@ -444,7 +444,7 @@ fun fo_term_for_combterm ctxt type_sys = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun aux top_level u = let val (head, args) = strip_combterm_comb u @@ -681,7 +681,7 @@ fun prepare_atp_problem ctxt readable_names explicit_forall type_sys explicit_apply hyp_ts concl_t facts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt type_sys hyp_ts concl_t facts (* Reordering these might or might not confuse the proof reconstruction diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Apr 16 16:15:37 2011 +0200 @@ -199,7 +199,7 @@ fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, (_, th))) = case struct_induct_rule_on th of SOME (p_name, ind_T) => - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T)) |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax)) end @@ -542,7 +542,7 @@ (fudge as {threshold_divisor, ridiculous_threshold, ...}) ({add, del, ...} : relevance_override) facts goal_ts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty val goal_const_tab = pconsts_in_terms thy is_built_in_const false (SOME false) goal_ts @@ -797,9 +797,9 @@ ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths chained_ths = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy - val local_facts = ProofContext.facts_of ctxt + val local_facts = Proof_Context.facts_of ctxt val named_locals = local_facts |> Facts.dest_static [] val assms = Assumption.all_assms_of ctxt fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms @@ -832,7 +832,7 @@ val backquote_thm = backquote o string_for_term ctxt o close_form o prop_of fun check_thms a = - case try (ProofContext.get_thms ctxt) a of + case try (Proof_Context.get_thms ctxt) a of NONE => false | SOME ths' => Thm.eq_thms (ths, ths') in @@ -887,7 +887,7 @@ max_relevant is_built_in_const fudge (override as {add, only, ...}) chained_ths hyp_ts concl_t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0), 1.0 / Real.fromInt (max_relevant + 1)) val add_ths = Attrib.eval_thms ctxt add diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Apr 16 16:15:37 2011 +0200 @@ -177,7 +177,7 @@ val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param fun default_raw_params ctxt = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in Data.get thy |> fold (AList.default (op =)) [("provers", [case !provers of @@ -332,7 +332,7 @@ Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => - let val ctxt = ProofContext.init_global thy in + let val ctxt = Proof_Context.init_global thy in writeln ("Default parameters for Sledgehammer:\n" ^ (case default_raw_params ctxt |> rev of [] => "none" diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Apr 16 16:15:37 2011 +0200 @@ -123,15 +123,15 @@ member (op =) (SMT_Solver.available_solvers_of ctxt) name fun is_prover_supported ctxt name = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name end fun is_prover_installed ctxt = - is_smt_prover ctxt orf is_atp_installed (ProofContext.theory_of ctxt) + is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt) fun default_max_relevant_for_prover ctxt name = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in if is_smt_prover ctxt name then SMT_Solver.default_max_relevant ctxt name else @@ -208,7 +208,7 @@ fun supported_provers ctxt = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = sort_strings (supported_atps thy) @ sort_strings (SMT_Solver.available_solvers_of ctxt) @@ -695,7 +695,7 @@ end fun get_prover ctxt auto name = - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in if is_smt_prover ctxt name then run_smt_solver auto name else if member (op =) (supported_atps thy) name then diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Apr 16 16:15:37 2011 +0200 @@ -180,7 +180,7 @@ val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug) val ctxt = Proof.context_of state - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val {facts = chained_ths, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i val no_dangerous_types = types_dangerous_types type_sys diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/TFL/post.ML Sat Apr 16 16:15:37 2011 +0200 @@ -136,7 +136,7 @@ fun simplify_defn strict thy cs ss congs wfs id pats def0 = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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)) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Sat Apr 16 16:15:37 2011 +0200 @@ -795,7 +795,7 @@ let val thy = Thm.theory_of_cterm ptm; val t = Thm.term_of ptm; - val ctxt = ProofContext.init_global thy |> Variable.auto_fixes t; + val ctxt = Proof_Context.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 da8817d01e7c -r 23f352990944 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Sat Apr 16 16:15:37 2011 +0200 @@ -357,7 +357,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_global sign)) + singleton (Syntax.check_terms (Proof_Context.init_global sign)) (Const("==",dummyT) $ Const(c,Ty) $ rhs); (*Make all TVars available for instantiation by adding a ? to the front*) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/arith_data.ML Sat Apr 16 16:15:37 2011 +0200 @@ -53,7 +53,7 @@ fun gen_arith_tac verbose ctxt = let - val tactics = Arith_Tactics.get (ProofContext.theory_of ctxt); + val tactics = Arith_Tactics.get (Proof_Context.theory_of ctxt); fun invoke (_, (name, tac)) k st = tac verbose ctxt k st; in FIRST' (map invoke (rev tactics)) end; diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/choice_specification.ML Sat Apr 16 16:15:37 2011 +0200 @@ -220,11 +220,11 @@ |> process_all (zip3 alt_names rew_imps frees) end - fun after_qed [[thm]] = ProofContext.background_theory (fn thy => + fun after_qed [[thm]] = Proof_Context.background_theory (fn thy => #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm)))); in thy - |> ProofContext.init_global + |> Proof_Context.init_global |> Variable.declare_term ex_prop |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]] end; diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Sat Apr 16 16:15:37 2011 +0200 @@ -258,7 +258,7 @@ fun make_under_quantifiers ctxt make t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun conv ctxt ct = case term_of ct of (t1 as Const _) $ (t2 as Abs _) => @@ -269,7 +269,7 @@ in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end fun make_nnf_thm_under_quantifiers ctxt = - make_under_quantifiers ctxt (make_nnf_thm (ProofContext.theory_of ctxt)) + make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt)) (* ------------------------------------------------------------------------- *) (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *) @@ -344,7 +344,7 @@ fun make_cnf_thm ctxt t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) = let val thm1 = make_cnf_thm_from_nnf x @@ -414,7 +414,7 @@ fun make_cnfx_thm ctxt t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val var_id = Unsynchronized.ref 0 (* properly initialized below *) fun new_free () = Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/code_evaluation.ML Sat Apr 16 16:15:37 2011 +0200 @@ -223,6 +223,6 @@ #> Code.datatype_interpretation ensure_term_of_code #> Code.abstype_interpretation ensure_abs_term_of_code #> Context.theory_map (Syntax.add_term_check 0 "termify" check_termify) - #> Value.add_evaluator ("code", dynamic_value_strict o ProofContext.theory_of); + #> Value.add_evaluator ("code", dynamic_value_strict o Proof_Context.theory_of); end; diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/enriched_type.ML --- a/src/HOL/Tools/enriched_type.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/enriched_type.ML Sat Apr 16 16:15:37 2011 +0200 @@ -41,7 +41,7 @@ (* type analysis *) fun term_with_typ ctxt T t = Envir.subst_term_types - (Type.typ_match (ProofContext.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t; + (Type.typ_match (Proof_Context.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t; fun find_atomic ctxt T = let @@ -186,7 +186,7 @@ let val coT = TFree var1 --> TFree var2; val contraT = TFree var2 --> TFree var1; - val sort = Sign.inter_sort (ProofContext.theory_of ctxt) (sort1, sort2); + val sort = Sign.inter_sort (Proof_Context.theory_of ctxt) (sort1, sort2); in consume (op =) coT ##>> consume (op =) contraT @@ -218,7 +218,7 @@ val qualify = Binding.qualify true prfx o Binding.name; fun mapper_declaration comp_thm id_thm phi context = let - val typ_instance = Type.typ_instance (ProofContext.tsig_of (Context.proof_of context)); + val typ_instance = Type.typ_instance (Proof_Context.tsig_of (Context.proof_of context)); val mapper' = Morphism.term phi mapper; val T_T' = pairself fastype_of (mapper, mapper'); in if typ_instance T_T' andalso typ_instance (swap T_T') diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/inductive.ML Sat Apr 16 16:15:37 2011 +0200 @@ -149,7 +149,7 @@ fun print_inductives ctxt = let val (tab, monos) = get_inductives ctxt; - val space = Consts.space_of (ProofContext.consts_of ctxt); + val space = Consts.space_of (Proof_Context.consts_of ctxt); in [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))), Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)] @@ -294,7 +294,7 @@ val concl = subst_bounds (frees, Logic.strip_assums_concl rule); val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule); val rule' = Logic.list_implies (prems, concl); - val aprems = map (atomize_term (ProofContext.theory_of ctxt)) prems; + val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems; val arule = list_all_free (params', Logic.list_implies (aprems, concl)); fun check_ind err t = case dest_predicate cs params t of @@ -375,7 +375,7 @@ (*Not ares_tac, since refl must be tried before any equality assumptions; backtracking may occur if the premises have extra variables!*) DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]) - |> singleton (ProofContext.export ctxt ctxt')) intr_ts + |> singleton (Proof_Context.export ctxt ctxt')) intr_ts in (intrs, unfold) end; @@ -421,7 +421,7 @@ REPEAT (FIRSTGOAL (eresolve_tac rules2)), EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))]) - |> singleton (ProofContext.export ctxt'' ctxt'''), + |> singleton (Proof_Context.export ctxt'' ctxt'''), map #2 c_intrs, length Ts) end @@ -487,7 +487,7 @@ THEN prove_intr2 last_c_intr end)) |> rulify - |> singleton (ProofContext.export ctxt' ctxt'') + |> singleton (Proof_Context.export ctxt' ctxt'') end; in map2 prove_eq cs elims @@ -510,7 +510,7 @@ fun mk_cases ctxt prop = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val ss = simpset_of ctxt; fun err msg = @@ -536,7 +536,7 @@ fun gen_inductive_cases prep_att prep_prop args lthy = let - val thy = ProofContext.theory_of lthy; + val thy = Proof_Context.theory_of lthy; val facts = args |> Par_List.map (fn ((a, atts), props) => ((a, map (prep_att thy) atts), Par_List.map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props)); @@ -555,7 +555,7 @@ val (_, ctxt') = Variable.add_fixes fixes ctxt; val props = Syntax.read_props ctxt' raw_props; val ctxt'' = fold Variable.declare_term props ctxt'; - val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props) + val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props) in Method.erule 0 rules end)) "dynamic case analysis on predicates"; @@ -563,7 +563,7 @@ fun mk_simp_eq ctxt prop = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ctxt' = Variable.auto_fixes prop ctxt val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of val substs = Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop) @@ -588,7 +588,7 @@ fun gen_inductive_simps prep_att prep_prop args lthy = let - val thy = ProofContext.theory_of lthy; + val thy = Proof_Context.theory_of lthy; val facts = args |> map (fn ((a, atts), props) => ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props)); @@ -603,7 +603,7 @@ fp_def rec_preds_defs ctxt ctxt''' = let val _ = clean_message quiet_mode " Proving the induction rule ..."; - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; (* predicates for induction rule *) @@ -702,7 +702,7 @@ rewrite_goals_tac simp_thms', atac 1])]) - in singleton (ProofContext.export ctxt'' ctxt''') (induct RS lemma) end; + in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end; @@ -779,7 +779,7 @@ (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) ||> Local_Theory.restore_naming lthy; val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) - (cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params))); + (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params))); val specs = if length cs < 2 then [] else @@ -801,7 +801,7 @@ val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'''; val (_, lthy'''') = Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, - ProofContext.export lthy''' lthy'' [mono]) lthy''; + Proof_Context.export lthy''' lthy'' [mono]) lthy''; in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs, list_comb (rec_const, params), preds, argTs, bs, xs) @@ -903,7 +903,7 @@ val raw_induct = zero_var_indexes (if no_ind then Drule.asm_rl else if coind then - singleton (ProofContext.export lthy2 lthy1) + singleton (Proof_Context.export lthy2 lthy1) (rotate_prems ~1 (Object_Logic.rulify (fold_rule rec_preds_defs (rewrite_rule simp_thms''' @@ -942,7 +942,7 @@ (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}) cnames_syn pnames spec monos lthy = let - val thy = ProofContext.theory_of lthy; + val thy = Proof_Context.theory_of lthy; val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); @@ -979,7 +979,7 @@ val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn'); val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs; val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs; - val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy; + val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy; fun close_rule r = list_all_free (rev (fold_aterms (fn t as Free (v as (s, _)) => @@ -998,7 +998,7 @@ fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy = let val ((vars, intrs), _) = lthy - |> ProofContext.set_mode ProofContext.mode_abbrev + |> Proof_Context.set_mode Proof_Context.mode_abbrev |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs; val (cs, ps) = chop (length cnames_syn) vars; val monos = Attrib.eval_thms lthy raw_monos; @@ -1020,7 +1020,7 @@ |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd |> Local_Theory.exit; val info = #2 (the_inductive ctxt' name); - in (info, ProofContext.theory_of ctxt') end; + in (info, Proof_Context.theory_of ctxt') end; (* read off arities of inductive predicates from raw induction rule *) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Sat Apr 16 16:15:37 2011 +0200 @@ -68,7 +68,7 @@ | NONE => (case rules of [] => - (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of + (case try (Inductive.the_inductive (Proof_Context.init_global thy)) s of SOME (_, {raw_induct, ...}) => length (Inductive.params_of raw_induct) | NONE => 0) @@ -86,7 +86,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_global thy)) s of + NONE => (case try (Inductive.the_inductive (Proof_Context.init_global thy)) s of NONE => NONE | SOME ({names, ...}, {intrs, raw_induct, ...}) => SOME (names, Codegen.thyname_of_const thy s, @@ -811,7 +811,7 @@ fun test_term ctxt [(t, [])] = let val t' = list_abs_free (Term.add_frees t [], t) - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val (xs, p) = strip_abs t'; val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs; val args = map Free args'; diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Sat Apr 16 16:15:37 2011 +0200 @@ -136,7 +136,7 @@ fun fun_of_prem thy rsets vs params rule ivs intr = let - val ctxt = ProofContext.init_global thy + val ctxt = Proof_Context.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) [])); @@ -483,7 +483,7 @@ fun add_ind_realizers name rsets thy = let val (_, {intrs, induct, raw_induct, elims, ...}) = - Inductive.the_inductive (ProofContext.init_global thy) name; + Inductive.the_inductive (Proof_Context.init_global thy) name; val vss = sort (int_ord o pairself length) (subsets (map fst (relevant_vars (concl_of (hd intrs))))) in diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/inductive_set.ML Sat Apr 16 16:15:37 2011 +0200 @@ -410,7 +410,7 @@ {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} cs intros monos params cnames_syn lthy = let - val thy = ProofContext.theory_of lthy; + val thy = Proof_Context.theory_of lthy; val {set_arities, pred_arities, to_pred_simps, ...} = PredSetConvData.get (Context.Proof lthy); fun infer (Abs (_, _, t)) = infer t diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/lin_arith.ML Sat Apr 16 16:15:37 2011 +0200 @@ -267,7 +267,7 @@ fun decomp ctxt : term -> decomp option = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val {discrete, inj_consts, ...} = get_arith_data ctxt in decomp_negation (thy, discrete, inj_consts) end; @@ -336,7 +336,7 @@ fun split_once_items ctxt (Ts : typ list, terms : term list) : (typ list * term list) list option = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt (* takes a list [t1, ..., tn] to the term *) (* tn' --> ... --> t1' --> False , *) (* where ti' = HOLogic.dest_Trueprop ti *) @@ -709,7 +709,7 @@ fun split_once_tac ss split_thms = let val ctxt = Simplifier.the_context ss - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val cond_split_tac = SUBGOAL (fn (subgoal, i) => let val Ts = rev (map snd (Logic.strip_params subgoal)) diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/list_to_set_comprehension.ML --- a/src/HOL/Tools/list_to_set_comprehension.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/list_to_set_comprehension.ML Sat Apr 16 16:15:37 2011 +0200 @@ -65,7 +65,7 @@ fun simproc ss redex = let val ctxt = Simplifier.the_context ss - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}] val set_singleton = @{lemma "set [a] = {x. x = a}" by simp} val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp} diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/primrec.ML Sat Apr 16 16:15:37 2011 +0200 @@ -225,7 +225,7 @@ val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs []; val tnames = distinct (op =) (map (#1 o snd) eqns); - val dts = find_dts (Datatype_Data.get_all (ProofContext.theory_of lthy)) tnames tnames; + val dts = find_dts (Datatype_Data.get_all (Proof_Context.theory_of lthy)) tnames tnames; val main_fns = map (fn (tname, {index, ...}) => (index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts; val {descr, rec_names, rec_rewrites, ...} = @@ -300,14 +300,14 @@ let val lthy = Named_Target.theory_init thy; val ((ts, simps), lthy') = add_primrec fixes specs lthy; - val simps' = ProofContext.export lthy' lthy simps; + val simps' = Proof_Context.export lthy' lthy simps; in ((ts, simps'), Local_Theory.exit_global lthy') end; fun add_primrec_overloaded ops fixes specs thy = let val lthy = Overloading.overloading ops thy; val ((ts, simps), lthy') = add_primrec fixes specs lthy; - val simps' = ProofContext.export lthy' lthy simps; + val simps' = Proof_Context.export lthy' lthy simps; in ((ts, simps'), Local_Theory.exit_global lthy') end; diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/recdef.ML Sat Apr 16 16:15:37 2011 +0200 @@ -160,7 +160,7 @@ fun prepare_hints thy opt_src = let - val ctxt0 = ProofContext.init_global thy; + val ctxt0 = Proof_Context.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_global thy; + val ctxt0 = Proof_Context.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_global thy) raw_congs; + val congs = eval_thms (Proof_Context.init_global thy) raw_congs; val (thy2, induct_rules) = tfl_fn thy congs name eqs; val ([induct_rules'], thy3) = thy2 @@ -252,7 +252,7 @@ fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i int lthy = let - val thy = ProofContext.theory_of lthy; + val thy = Proof_Context.theory_of lthy; val name = prep_name thy raw_name; val atts = map (prep_att thy) raw_atts; val tcs = diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/record.ML Sat Apr 16 16:15:37 2011 +0200 @@ -109,8 +109,8 @@ fun do_typedef raw_tyco repT raw_vs thy = let - val ctxt = ProofContext.init_global thy |> Variable.declare_typ repT; - val vs = map (ProofContext.check_tfree ctxt) raw_vs; + val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT; + val vs = map (Proof_Context.check_tfree ctxt) raw_vs; val tac = Tactic.rtac UNIV_witness 1; in thy @@ -680,7 +680,7 @@ fun record_field_types_tr more ctxt t = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]); fun split_args (field :: fields) ((name, arg) :: fargs) = @@ -693,7 +693,7 @@ | split_args _ _ = ([], []); fun mk_ext (fargs as (name, _) :: _) = - (case get_fieldext thy (ProofContext.intern_const ctxt name) of + (case get_fieldext thy (Proof_Context.intern_const ctxt name) of SOME (ext, alphas) => (case get_extfields thy ext of SOME fields => @@ -739,7 +739,7 @@ fun record_fields_tr more ctxt t = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; fun err msg = raise TERM ("Error in record input: " ^ msg, [t]); fun split_args (field :: fields) ((name, arg) :: fargs) = @@ -753,7 +753,7 @@ | split_args _ _ = ([], []); fun mk_ext (fargs as (name, _) :: _) = - (case get_fieldext thy (ProofContext.intern_const ctxt name) of + (case get_fieldext thy (Proof_Context.intern_const ctxt name) of SOME (ext, _) => (case get_extfields thy ext of SOME fields => @@ -814,7 +814,7 @@ fun record_type_tr' ctxt t = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val T = decode_type thy t; val varifyT = varifyT (Term.maxidx_of_typ T); @@ -831,7 +831,7 @@ (let val (f :: fs, _) = split_last fields; val fields' = - apfst (ProofContext.extern_const ctxt) f :: + apfst (Proof_Context.extern_const ctxt) f :: map (apfst Long_Name.base_name) fs; val (args', more) = split_last args; val alphavars = map varifyT (#1 (split_last alphas)); @@ -861,7 +861,7 @@ the (nested) extension types*) fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val T = decode_type thy tm; val midx = maxidx_of_typ T; val varifyT = varifyT midx; @@ -914,7 +914,7 @@ fun record_tr' ctxt t = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; fun strip_fields t = (case strip_comb t of @@ -925,7 +925,7 @@ SOME fields => (let val (f :: fs, _) = split_last (map fst fields); - val fields' = ProofContext.extern_const ctxt f :: map Long_Name.base_name fs; + val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs; val (args', more) = split_last args; in (fields' ~~ args') @ strip_fields more end handle ListPair.UnequalLengths => [("", t)]) @@ -957,7 +957,7 @@ fun dest_update ctxt c = (case try Lexicon.unmark_const c of - SOME d => try (unsuffix updateN) (ProofContext.extern_const ctxt d) + SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d) | NONE => NONE); fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) = @@ -997,7 +997,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_global thy) (Goal.fork prf) prop + Goal.future_result (Proof_Context.init_global thy) (Goal.fork prf) prop else prf () in Drule.export_without_context thm end; @@ -1007,7 +1007,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_global thy) [] asms prop tac; + val prf = prv (Proof_Context.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; @@ -1040,7 +1040,7 @@ else mk_comp_id acc; val prop = lhs === rhs; val othm = - Goal.prove (ProofContext.init_global thy) [] [] prop + Goal.prove (Proof_Context.init_global thy) [] [] prop (fn _ => simp_tac defset 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN @@ -1064,7 +1064,7 @@ else HOLogic.mk_comp (u' $ f', u $ f); val prop = lhs === rhs; val othm = - Goal.prove (ProofContext.init_global thy) [] [] prop + Goal.prove (Proof_Context.init_global thy) [] [] prop (fn _ => simp_tac defset 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN @@ -1105,7 +1105,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_global thy) [] [] prop' + Goal.prove (Proof_Context.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)) @@ -1197,7 +1197,7 @@ val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)]; val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv); in - Goal.prove (ProofContext.init_global thy) [] [] prop + Goal.prove (Proof_Context.init_global thy) [] [] prop (fn _ => simp_tac simpset 1 THEN REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN @@ -1525,7 +1525,7 @@ fun cert_typ ctxt raw_T env = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg; val env' = OldTerm.add_typ_tfrees (T, env); @@ -2392,7 +2392,7 @@ fun read_parent NONE ctxt = (NONE, ctxt) | read_parent (SOME raw_T) ctxt = - (case ProofContext.read_typ_abbrev ctxt raw_T of + (case Proof_Context.read_typ_abbrev ctxt raw_T of Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt) | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); @@ -2413,8 +2413,8 @@ if quiet_mode then () else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ..."); - val ctxt = ProofContext.init_global thy; - fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T) + val ctxt = Proof_Context.init_global thy; + fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T) handle TYPE (msg, _, _) => error msg; @@ -2463,12 +2463,12 @@ fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.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; val (fields, ctxt3) = fold_map read_field raw_fields ctxt2; - val params' = map (ProofContext.check_tfree ctxt3) params; + val params' = map (Proof_Context.check_tfree ctxt3) params; in thy |> add_record quiet_mode (params', binding) parent fields end; end; diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/refute.ML Sat Apr 16 16:15:37 2011 +0200 @@ -224,7 +224,7 @@ parameters = Symtab.merge (op =) (pa1, pa2)}; ); -val get_data = Data.get o ProofContext.theory_of; +val get_data = Data.get o Proof_Context.theory_of; (* ------------------------------------------------------------------------- *) @@ -683,7 +683,7 @@ fun collect_axioms ctxt t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val _ = tracing "Adding axioms..." val axioms = Theory.all_axioms_of thy fun collect_this_axiom (axname, ax) axs = @@ -858,7 +858,7 @@ fun ground_types ctxt t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun collect_types T acc = (case T of Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc) @@ -1049,7 +1049,7 @@ {sizes, minsize, maxsize, maxvars, maxtime, satsolver, no_assms, expect} assm_ts t negate = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt (* string -> unit *) fun check_expect outcome_code = if expect = "" orelse outcome_code = expect then () @@ -1548,7 +1548,7 @@ fun stlc_interpreter ctxt model args t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val (typs, terms) = model val {maxvars, def_eq, next_idx, bounds, wellformed} = args (* Term.typ -> (interpretation * model * arguments) option *) @@ -1836,7 +1836,7 @@ fun IDT_interpreter ctxt model args t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val (typs, terms) = model (* Term.typ -> (interpretation * model * arguments) option *) fun interpret_term (Type (s, Ts)) = @@ -1929,7 +1929,7 @@ fun IDT_constructor_interpreter ctxt model args t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt (* returns a list of canonical representations for terms of the type 'T' *) (* It would be nice if we could just use 'print' for this, but 'print' *) (* for IDTs calls 'IDT_constructor_interpreter' again, and this could *) @@ -2194,7 +2194,7 @@ fun IDT_recursion_interpreter ctxt model args t = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt in (* careful: here we descend arbitrarily deep into 't', possibly before *) (* any other interpreter for atomic terms has had a chance to look at *) @@ -3022,7 +3022,7 @@ fun IDT_printer ctxt model T intr assignment = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt in (case T of Type (s, Ts) => @@ -3189,7 +3189,7 @@ let val thy' = fold set_default_param parms thy; val output = - (case get_default_params (ProofContext.init_global thy') of + (case get_default_params (Proof_Context.init_global thy') of [] => "none" | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults)); val _ = writeln ("Default parameters for 'refute':\n" ^ output); diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/transfer.ML Sat Apr 16 16:15:37 2011 +0200 @@ -118,7 +118,7 @@ |> Variable.declare_thm thm |> Variable.declare_term (term_of a) |> Variable.declare_term (term_of D); - val certify = Thm.cterm_of (ProofContext.theory_of ctxt3); + val certify = Thm.cterm_of (Proof_Context.theory_of ctxt3); val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []); val c_vars = map (certify o Var) vars; diff -r da8817d01e7c -r 23f352990944 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/Tools/typedef.ML Sat Apr 16 16:15:37 2011 +0200 @@ -149,7 +149,7 @@ (* lhs *) - val args = map (ProofContext.check_tfree tmp_ctxt') raw_args; + val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args; val (newT, typedecl_lthy) = lthy |> Typedecl.typedecl (tname, args, mx) ||> Variable.declare_term set; @@ -179,17 +179,17 @@ val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = let - val thy = ProofContext.theory_of set_lthy; + val thy = Proof_Context.theory_of set_lthy; val cert = Thm.cterm_of thy; val (defs, A) = - Local_Defs.export_cterm set_lthy (ProofContext.init_global thy) (cert set') + Local_Defs.export_cterm set_lthy (Proof_Context.init_global thy) (cert set') ||> Thm.term_of; val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |> Local_Theory.background_theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A); - val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy); + val cert = Thm.cterm_of (Proof_Context.theory_of axiom_lthy); val typedef = Local_Defs.contract axiom_lthy defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom; in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end; @@ -207,7 +207,7 @@ fun typedef_result inhabited lthy1 = let - val cert = Thm.cterm_of (ProofContext.theory_of lthy1); + val cert = Thm.cterm_of (Proof_Context.theory_of lthy1); val inhabited' = Local_Defs.contract lthy1 (the_list set_def) (cert (mk_inhabited set')) inhabited; val typedef' = inhabited' RS typedef; diff -r da8817d01e7c -r 23f352990944 src/HOL/ex/Iff_Oracle.thy --- a/src/HOL/ex/Iff_Oracle.thy Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/ex/Iff_Oracle.thy Sat Apr 16 16:15:37 2011 +0200 @@ -54,7 +54,7 @@ method_setup iff = {* Scan.lift Parse.nat >> (fn n => fn ctxt => SIMPLE_METHOD - (HEADGOAL (rtac (iff_oracle (ProofContext.theory_of ctxt, n))) + (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n))) handle Fail _ => no_tac)) *} "iff oracle" diff -r da8817d01e7c -r 23f352990944 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Sat Apr 16 16:15:37 2011 +0200 @@ -55,7 +55,7 @@ fun thms_of_name ctxt name = let val lex = Keyword.get_lexicons - val get = maps (ProofContext.get_fact ctxt o fst) + val get = maps (Proof_Context.get_fact ctxt o fst) in Source.of_string name |> Symbol.source @@ -77,7 +77,7 @@ fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val timeout = Time.fromSeconds 30 val xs = run_atp force_full_types timeout i i ctxt th atp in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end diff -r da8817d01e7c -r 23f352990944 src/Provers/Arith/cancel_sums.ML --- a/src/Provers/Arith/cancel_sums.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Provers/Arith/cancel_sums.ML Sat Apr 16 16:15:37 2011 +0200 @@ -61,7 +61,7 @@ NONE => NONE | SOME bal => let - val thy = ProofContext.theory_of (Simplifier.the_context ss); + val thy = Proof_Context.theory_of (Simplifier.the_context ss); val (ts, us) = pairself (sort Term_Ord.term_ord o Data.dest_sum) bal; val (ts', us', vs) = cancel ts us []; in diff -r da8817d01e7c -r 23f352990944 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat Apr 16 16:15:37 2011 +0200 @@ -168,7 +168,7 @@ fun number_of ctxt = (case Data.get (Context.Proof ctxt) of - {number_of = SOME f, ...} => f (ProofContext.theory_of ctxt) + {number_of = SOME f, ...} => f (Proof_Context.theory_of ctxt) | _ => fn _ => fn _ => raise CTERM ("number_of", [])); @@ -474,7 +474,7 @@ fun mkthm ss asms (just: injust) = let val ctxt = Simplifier.the_context ss; - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt; val number_of = number_of ctxt; val simpset' = Simplifier.inherit_context ss simpset; @@ -895,7 +895,7 @@ fun prover ss thms Tconcl (js : injust list) split_neq pos : thm option = let val ctxt = Simplifier.the_context ss - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val nTconcl = LA_Logic.neg_prop Tconcl val cnTconcl = cterm_of thy nTconcl val nTconclthm = Thm.assume cnTconcl diff -r da8817d01e7c -r 23f352990944 src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Provers/classical.ML Sat Apr 16 16:15:37 2011 +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_global (Thm.theory_of_thm rl); + val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl); in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end; @@ -850,13 +850,13 @@ val get_global_claset = #1 o GlobalClaset.get; val map_global_claset = GlobalClaset.map o apfst; -val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of; +val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of; fun map_context_cs f = GlobalClaset.map (apsnd (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers)))); fun global_claset_of thy = let val (cs, ctxt_cs) = GlobalClaset.get thy - in context_cs (ProofContext.init_global thy) cs (ctxt_cs) end; + in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end; (* context dependent components *) diff -r da8817d01e7c -r 23f352990944 src/Provers/order.ML --- a/src/Provers/order.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Provers/order.ML Sat Apr 16 16:15:37 2011 +0200 @@ -1225,7 +1225,7 @@ in SUBGOAL (fn (A, n) => fn st => let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A) val C = subst_bounds (rfrees, Logic.strip_assums_concl A) diff -r da8817d01e7c -r 23f352990944 src/Provers/quantifier1.ML --- a/src/Provers/quantifier1.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Provers/quantifier1.ML Sat Apr 16 16:15:37 2011 +0200 @@ -113,7 +113,7 @@ in exqu [] end; fun prove_conv tac thy tu = - let val ctxt = ProofContext.init_global thy; + let val ctxt = Proof_Context.init_global thy; val eq_tu = Logic.mk_equals tu; val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt; val thm = Goal.prove ctxt' [] [] fixed_goal diff -r da8817d01e7c -r 23f352990944 src/Provers/quasi.ML --- a/src/Provers/quasi.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Provers/quasi.ML Sat Apr 16 16:15:37 2011 +0200 @@ -553,7 +553,7 @@ fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st => let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); val C = subst_bounds (rfrees, Logic.strip_assums_concl A); @@ -574,7 +574,7 @@ fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A)); val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A); val C = subst_bounds (rfrees, Logic.strip_assums_concl A); diff -r da8817d01e7c -r 23f352990944 src/Provers/trancl.ML --- a/src/Provers/trancl.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Provers/trancl.ML Sat Apr 16 16:15:37 2011 +0200 @@ -534,7 +534,7 @@ fun trancl_tac ctxt = SUBGOAL (fn (A, n) => fn st => let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val Hs = Logic.strip_assums_hyp A; val C = Logic.strip_assums_concl A; val (rel, subgoals, prf) = mkconcl_trancl C; @@ -553,7 +553,7 @@ fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st => let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val Hs = Logic.strip_assums_hyp A; val C = Logic.strip_assums_concl A; val (rel, subgoals, prf) = mkconcl_rtrancl C; diff -r da8817d01e7c -r 23f352990944 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/Code/code_preproc.ML Sat Apr 16 16:15:37 2011 +0200 @@ -90,7 +90,7 @@ fun add_unfold_post raw_thm thy = let - val thm = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) raw_thm; + val thm = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy) raw_thm; val thm_sym = Thm.symmetric thm; in thy |> map_pre_post (fn (pre, post) => @@ -165,7 +165,7 @@ fun preprocess_conv thy = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy; in Simplifier.rewrite pre @@ -186,7 +186,7 @@ fun print_codeproc thy = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.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 da8817d01e7c -r 23f352990944 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/Code/code_runtime.ML Sat Apr 16 16:15:37 2011 +0200 @@ -83,14 +83,14 @@ fun reject_vars thy t = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end; fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target); fun evaluation cookie thy evaluator vs_t args = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; val (program_code, value_name) = evaluator vs_t; val value_code = space_implode " " (value_name :: "()" :: map (enclose "(" ")") args); @@ -188,7 +188,7 @@ fun evaluation_code thy module_name tycos consts = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts; val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; val (ml_code, target_names) = @@ -202,7 +202,7 @@ | SOME const'' => (const, const'')) consts consts'' val tycos_map = map2 (fn tyco => fn NONE => - error ("Type " ^ quote (ProofContext.extern_type ctxt tyco) ^ + error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^ "\nhas a user-defined serialization") | SOME tyco'' => (tyco, tyco'')) tycos tycos''; in (ml_code, (tycos_map, consts_map)) end; @@ -227,7 +227,7 @@ val tycos' = fold (insert (op =)) new_tycos tycos; val consts' = fold (insert (op =)) new_consts consts; val acc_code = Lazy.lazy (fn () => - evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts' + evaluation_code (Proof_Context.theory_of ctxt) "Code" tycos' consts' |> apsnd snd); in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end; @@ -245,7 +245,7 @@ fun ml_code_antiq raw_const background = let - val const = Code.check_const (ProofContext.theory_of background) raw_const; + val const = Code.check_const (Proof_Context.theory_of background) raw_const; val is_first = is_first_occ background; val background' = register_const const background; in (print_code is_first const, background') end; diff -r da8817d01e7c -r 23f352990944 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/Code/code_simp.ML Sat Apr 16 16:15:37 2011 +0200 @@ -59,9 +59,9 @@ fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy; val setup = Method.setup (Binding.name "code_simp") - (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o ProofContext.theory_of))) + (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of))) "simplification with code equations" - #> Value.add_evaluator ("simp", dynamic_value o ProofContext.theory_of); + #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of); (* evaluation with static code context *) diff -r da8817d01e7c -r 23f352990944 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/Code/code_target.ML Sat Apr 16 16:15:37 2011 +0200 @@ -307,7 +307,7 @@ fun project_program thy abortable names_hidden names1 program2 = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; val names2 = subtract (op =) names_hidden names1; val program3 = Graph.subgraph (not o member (op =) names_hidden) program2; val names4 = Graph.all_succs program3 names2; @@ -316,7 +316,7 @@ val _ = if null empty_funs then () else error ("No code equations for " ^ - commas (map (ProofContext.extern_const ctxt) empty_funs)); + commas (map (Proof_Context.extern_const ctxt) empty_funs)); val program4 = Graph.subgraph (member (op =) names4) program3; in (names4, program4) end; @@ -515,7 +515,7 @@ (parse_const_terms -- Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances) -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int))) (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) => - let val thy = ProofContext.theory_of ctxt in + let val thy = Proof_Context.theory_of ctxt in present_code thy (mk_cs thy) (fn naming => maps (fn f => f thy naming) mk_stmtss) target some_width "Example" [] diff -r da8817d01e7c -r 23f352990944 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/Code/code_thingol.ML Sat Apr 16 16:15:37 2011 +0200 @@ -490,18 +490,18 @@ | _ => []; fun labelled_name thy program name = - let val ctxt = ProofContext.init_global thy in + let val ctxt = Proof_Context.init_global thy in case Graph.get_node program name of Fun (c, _) => quote (Code.string_of_const thy c) - | Datatype (tyco, _) => "type " ^ quote (ProofContext.extern_type ctxt tyco) + | Datatype (tyco, _) => "type " ^ quote (Proof_Context.extern_type ctxt tyco) | Datatypecons (c, _) => quote (Code.string_of_const thy c) - | Class (class, _) => "class " ^ quote (ProofContext.extern_class ctxt class) + | Class (class, _) => "class " ^ quote (Proof_Context.extern_class ctxt class) | Classrel (sub, super) => let val Class (sub, _) = Graph.get_node program sub; val Class (super, _) = Graph.get_node program super; in - quote (ProofContext.extern_class ctxt sub ^ " < " ^ ProofContext.extern_class ctxt super) + quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super) end | Classparam (c, _) => quote (Code.string_of_const thy c) | Classinst ((class, (tyco, _)), _) => @@ -509,7 +509,7 @@ val Class (class, _) = Graph.get_node program class; val Datatype (tyco, _) = Graph.get_node program tyco; in - quote (ProofContext.extern_type ctxt tyco ^ " :: " ^ ProofContext.extern_class ctxt class) + quote (Proof_Context.extern_type ctxt tyco ^ " :: " ^ Proof_Context.extern_class ctxt class) end end; diff -r da8817d01e7c -r 23f352990944 src/Tools/WWW_Find/find_theorems.ML --- a/src/Tools/WWW_Find/find_theorems.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/WWW_Find/find_theorems.ML Sat Apr 16 16:15:37 2011 +0200 @@ -207,7 +207,7 @@ fun do_find () = let - val ctxt = ProofContext.init_global (Thy_Info.get_theory thy_name); + val ctxt = Proof_Context.init_global (Thy_Info.get_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 da8817d01e7c -r 23f352990944 src/Tools/adhoc_overloading.ML --- a/src/Tools/adhoc_overloading.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/adhoc_overloading.ML Sat Apr 16 16:15:37 2011 +0200 @@ -89,7 +89,7 @@ fun unifiable_with ctxt T1 (c, T2) = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val maxidx1 = Term.maxidx_of_typ T1; val T2' = Logic.incr_tvar (maxidx1 + 1) T2; val maxidx2 = Int.max (maxidx1, Term.maxidx_of_typ T2'); @@ -100,14 +100,14 @@ fun insert_internal_same ctxt t (Const (c, T)) = (case map_filter (unifiable_with ctxt T) - (Same.function (get_variants (ProofContext.theory_of ctxt)) c) of + (Same.function (get_variants (Proof_Context.theory_of ctxt)) c) of [] => unresolved_err ctxt (c, T) t "no instances" | [c'] => Const (c', dummyT) | _ => raise Same.SAME) | insert_internal_same _ _ _ = raise Same.SAME; fun insert_external_same ctxt _ (Const (c, T)) = - Const (Same.function (get_external (ProofContext.theory_of ctxt)) c, T) + Const (Same.function (get_external (Proof_Context.theory_of ctxt)) c, T) | insert_external_same _ _ _ = raise Same.SAME; fun gen_check_uncheck replace ts ctxt = @@ -121,7 +121,7 @@ fun reject_unresolved ts ctxt = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; fun check_unresolved t = case filter (is_overloaded thy o fst) (Term.add_consts t []) of [] => () diff -r da8817d01e7c -r 23f352990944 src/Tools/atomize_elim.ML --- a/src/Tools/atomize_elim.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/atomize_elim.ML Sat Apr 16 16:15:37 2011 +0200 @@ -115,7 +115,7 @@ fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) => let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val _ $ thesis = Logic.strip_assums_concl subg (* Introduce a quantifier first if the thesis is not bound *) diff -r da8817d01e7c -r 23f352990944 src/Tools/case_product.ML --- a/src/Tools/case_product.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/case_product.ML Sat Apr 16 16:15:37 2011 +0200 @@ -74,7 +74,7 @@ (Tactic.rtac (thm1 OF p_cons1) THEN' EVERY' (map (fn p => Tactic.rtac thm2' - THEN' EVERY' (map (ProofContext.fact_tac o single) p)) premss) + THEN' EVERY' (map (Proof_Context.fact_tac o single) p)) premss) ) end diff -r da8817d01e7c -r 23f352990944 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/coherent.ML Sat Apr 16 16:15:37 2011 +0200 @@ -82,7 +82,7 @@ | valid_conj ctxt facts env (t :: ts) = Seq.maps (fn (u, x) => Seq.map (apsnd (cons x)) (valid_conj ctxt facts - (Pattern.match (ProofContext.theory_of ctxt) (t, u) env) ts + (Pattern.match (Proof_Context.theory_of ctxt) (t, u) env) ts handle Pattern.MATCH => Seq.empty)) (Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t))); @@ -219,7 +219,7 @@ (mk_dom xs) Net.empty 0 0 of NONE => no_tac | SOME prf => - rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1 + rtac (thm_of_cl_prf (Proof_Context.theory_of context) concl [] prf) 1 end) context 1) ctxt; val setup = Method.setup @{binding coherent} diff -r da8817d01e7c -r 23f352990944 src/Tools/induct.ML --- a/src/Tools/induct.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/induct.ML Sat Apr 16 16:15:37 2011 +0200 @@ -128,7 +128,7 @@ Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv Conv.rewr_conv Drule.swap_prems_eq -fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt); +fun drop_judgment ctxt = Object_Logic.drop_judgment (Proof_Context.theory_of ctxt); fun find_eq ctxt t = let @@ -386,7 +386,7 @@ fun prep_inst ctxt align tune (tm, ts) = let - val cert = Thm.cterm_of (ProofContext.theory_of ctxt); + val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); fun prep_var (x, SOME t) = let val cx = cert x; @@ -470,7 +470,7 @@ fun cases_tac ctxt simp insts opt_rule facts = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; fun inst_rule r = (if null insts then r @@ -573,7 +573,7 @@ fun guess_instance ctxt rule i st = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val maxidx = Thm.maxidx_of st; val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal)); @@ -599,7 +599,7 @@ fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] = let - val x = Name.clean (ProofContext.revert_skolem ctxt z); + val x = Name.clean (Proof_Context.revert_skolem ctxt z); fun index i [] = [] | index i (y :: ys) = if x = y then x ^ string_of_int i :: index (i + 1) ys @@ -640,13 +640,13 @@ fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) => let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val cert = Thm.cterm_of thy; val v = Free (x, T); fun spec_rule prfx (xs, body) = @{thm Pure.meta_spec} - |> Thm.rename_params_rule ([Name.clean (ProofContext.revert_skolem ctxt x)], 1) + |> Thm.rename_params_rule ([Name.clean (Proof_Context.revert_skolem ctxt x)], 1) |> Thm.lift_rule (cert prfx) |> `(Thm.prop_of #> Logic.strip_assums_concl) |-> (fn pred $ arg => @@ -722,7 +722,7 @@ fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; val atomized_defs = map (map (Conv.fconv_rule atomize_cterm)) defs; @@ -777,7 +777,7 @@ |> Seq.maps (fn rule' => CASES (rule_cases ctxt rule' cases) (Tactic.rtac rule' i THEN - PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) + PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) THEN_ALL_NEW_CASES ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac) @@ -809,7 +809,7 @@ fun coinduct_tac ctxt inst taking opt_rule facts = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; fun inst_rule r = if null inst then `Rule_Cases.get r diff -r da8817d01e7c -r 23f352990944 src/Tools/induct_tacs.ML --- a/src/Tools/induct_tacs.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/induct_tacs.ML Sat Apr 16 16:15:37 2011 +0200 @@ -34,7 +34,7 @@ SOME rule => rule | NONE => (case Induct.find_casesT ctxt - (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of + (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s))) of rule :: _ => rule | [] => @{thm case_split})); val _ = Method.trace ctxt [rule]; diff -r da8817d01e7c -r 23f352990944 src/Tools/interpretation_with_defs.ML --- a/src/Tools/interpretation_with_defs.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/interpretation_with_defs.ML Sat Apr 16 16:15:37 2011 +0200 @@ -42,7 +42,7 @@ expression raw_defs raw_eqns theory = let val (_, (_, defs_ctxt)) = - prep_decl expression I [] (ProofContext.init_global theory); + prep_decl expression I [] (Proof_Context.init_global theory); val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs |> Syntax.check_terms defs_ctxt; @@ -56,7 +56,7 @@ |> Local_Theory.exit_result_global (map o Morphism.thm); val ((propss, deps, export), expr_ctxt) = theory' - |> ProofContext.init_global + |> Proof_Context.init_global |> prep_expr expression; val eqns = map (parse_prop expr_ctxt o snd) raw_eqns @@ -66,7 +66,7 @@ val export' = Variable.export_morphism goal_ctxt expr_ctxt; fun after_qed witss eqns = - (ProofContext.background_theory o Context.theory_map) + (Proof_Context.background_theory o Context.theory_map) (note_eqns_register deps witss def_eqns attrss eqns export export'); in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end; diff -r da8817d01e7c -r 23f352990944 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/misc_legacy.ML Sat Apr 16 16:15:37 2011 +0200 @@ -26,9 +26,9 @@ fun simple_read_term thy T s = let - val ctxt = ProofContext.init_global thy - |> ProofContext.allow_dummies - |> ProofContext.set_mode ProofContext.mode_schematic; + val ctxt = Proof_Context.init_global thy + |> Proof_Context.allow_dummies + |> Proof_Context.set_mode Proof_Context.mode_schematic; val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term; in parse ctxt s |> Type.constraint T |> Syntax.check_term ctxt end; diff -r da8817d01e7c -r 23f352990944 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/nbe.ML Sat Apr 16 16:15:37 2011 +0200 @@ -389,7 +389,7 @@ fun compile_eqnss thy nbe_program raw_deps [] = [] | compile_eqnss thy nbe_program raw_deps eqnss = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; val (deps, deps_vals) = split_list (map_filter (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps); val idx_of = raw_deps @@ -615,7 +615,7 @@ (** setup **) -val setup = Value.add_evaluator ("nbe", dynamic_value o ProofContext.theory_of); +val setup = Value.add_evaluator ("nbe", dynamic_value o Proof_Context.theory_of); end; \ No newline at end of file diff -r da8817d01e7c -r 23f352990944 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/quickcheck.ML Sat Apr 16 16:15:37 2011 +0200 @@ -329,7 +329,7 @@ fun test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) ts = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt fun message s = if Config.get ctxt quiet then () else Output.urgent_message s val (ts', eval_terms) = split_list ts val _ = map check_test_term ts' @@ -400,7 +400,7 @@ fun test_goal_terms lthy (limit_time, is_interactive) insts check_goals = let fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) - val thy = ProofContext.theory_of lthy + val thy = Proof_Context.theory_of lthy val default_insts = if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy) val inst_goals = @@ -568,7 +568,7 @@ | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg) | parse_test_param ("default_type", arg) = (fn gen_ctxt => map_test_params - ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt) + ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt) | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg) | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg)) | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg) @@ -583,9 +583,9 @@ else error ("Unknown tester or test parameter: " ^ name); fun parse_test_param_inst (name, arg) ((insts, eval_terms), ctxt) = - case try (ProofContext.read_typ ctxt) name + case try (Proof_Context.read_typ ctxt) name of SOME (TFree (v, _)) => - ((AList.update (op =) (v, ProofContext.read_typ ctxt (the_single arg)) insts, eval_terms), ctxt) + ((AList.update (op =) (v, Proof_Context.read_typ ctxt (the_single arg)) insts, eval_terms), ctxt) | NONE => (case name of "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), ctxt) | _ => ((insts, eval_terms), Context.proof_map (parse_test_param (name, arg)) ctxt)); diff -r da8817d01e7c -r 23f352990944 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/subtyping.ML Sat Apr 16 16:15:37 2011 +0200 @@ -97,7 +97,7 @@ fun unify weak ctxt = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; val pp = Syntax.pp ctxt; val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy); @@ -279,7 +279,7 @@ let val coes_graph = coes_graph_of ctxt; val tmaps = tmaps_of ctxt; - val tsig = Sign.tsig_of (ProofContext.theory_of ctxt); + val tsig = Sign.tsig_of (Proof_Context.theory_of ctxt); val pp = Syntax.pp ctxt; val arity_sorts = Type.arity_sorts pp tsig; val subsort = Type.subsort tsig; @@ -718,8 +718,8 @@ fun coercion_infer_types ctxt = infer_types ctxt - (try (Consts.the_constraint (ProofContext.consts_of ctxt))) - (ProofContext.def_type ctxt); + (try (Consts.the_constraint (Proof_Context.consts_of ctxt))) + (Proof_Context.def_type ctxt); val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false); diff -r da8817d01e7c -r 23f352990944 src/Tools/value.ML --- a/src/Tools/value.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/Tools/value.ML Sat Apr 16 16:15:37 2011 +0200 @@ -26,11 +26,11 @@ val add_evaluator = Evaluator.map o AList.update (op =); fun value_select name ctxt = - case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name + case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name of NONE => error ("No such evaluator: " ^ name) | SOME f => f ctxt; -fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt) +fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt) in if null evaluators then error "No evaluators" else let val (evaluators, (_, evaluator)) = split_last evaluators in case get_first (fn (_, f) => try (f ctxt) t) evaluators diff -r da8817d01e7c -r 23f352990944 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/ZF/Tools/datatype_package.ML Sat Apr 16 16:15:37 2011 +0200 @@ -402,7 +402,7 @@ fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.init_global thy; fun read_is strs = map (Syntax.parse_term ctxt #> Type.constraint @{typ i}) strs |> Syntax.check_terms ctxt; diff -r da8817d01e7c -r 23f352990944 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/ZF/Tools/ind_cases.ML Sat Apr 16 16:15:37 2011 +0200 @@ -30,7 +30,7 @@ fun smart_cases ctxt s = let - val thy = ProofContext.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; fun err msg = cat_error msg ("Malformed set membership statement: " ^ s); val A = Syntax.read_prop ctxt s handle ERROR msg => err msg; val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop @@ -46,7 +46,7 @@ fun inductive_cases args thy = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.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 da8817d01e7c -r 23f352990944 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/ZF/Tools/induct_tacs.ML Sat Apr 16 16:15:37 2011 +0200 @@ -91,7 +91,7 @@ fun exhaust_induct_tac exh ctxt var i state = let - val thy = ProofContext.theory_of ctxt + val thy = Proof_Context.theory_of ctxt val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state val tn = find_tname ctxt' var (map term_of asms) val rule = @@ -166,7 +166,7 @@ fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy = let - val ctxt = ProofContext.init_global thy; + val ctxt = Proof_Context.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 da8817d01e7c -r 23f352990944 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sat Apr 16 15:47:52 2011 +0200 +++ b/src/ZF/Tools/inductive_package.ML Sat Apr 16 16:15:37 2011 +0200 @@ -60,7 +60,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_global thy; + val ctxt = Proof_Context.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); @@ -143,7 +143,7 @@ If no mutual recursion then it equals the one recursive set. If mutual recursion then it differs from all the recursive sets. *) val big_rec_base_name = space_implode "_" rec_base_names; - val big_rec_name = ProofContext.intern_const ctxt big_rec_base_name; + val big_rec_name = Proof_Context.intern_const ctxt big_rec_base_name; val _ = @@ -173,7 +173,7 @@ |> Sign.add_path big_rec_base_name |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs); - val ctxt1 = ProofContext.init_global thy1; + val ctxt1 = Proof_Context.init_global thy1; (*fetch fp definitions from the theory*) @@ -260,7 +260,7 @@ THEN (PRIMITIVE (fold_rule part_rec_defs)); (*Elimination*) - val elim = rule_by_tactic (ProofContext.init_global thy1) basic_elim_tac + val elim = rule_by_tactic (Proof_Context.init_global thy1) basic_elim_tac (unfold RS Ind_Syntax.equals_CollectD) (*Applies freeness of the given constructors, which *must* be unfolded by @@ -553,7 +553,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_global thy; + val ctxt = Proof_Context.init_global thy; val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT) #> Syntax.check_terms ctxt;