--- 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}
--- 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
--- 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}%
--- 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%
--- 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)
--- 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 =
--- 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];
--- 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 =
--- 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
--- 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
--- 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
--- 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"}
--- 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;
*}
--- 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);
--- 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)
--- 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*)
--- 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*)
--- 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*)
--- 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"
--- 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
--- 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])
--- 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
--- 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
--- 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
--- 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
--- 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)
--- 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)
--- 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
--- 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)
--- 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
--- 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)
--- 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
--- 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
--- 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' =
--- 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
--- 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);
--- 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: *)
(*
--- 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;
--- 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 \<bullet> (pi2 \<bullet> 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
--- 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";
--- 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)
--- 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 |>
--- 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'' |>
--- 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
--- 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 *)
--- 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:",
--- 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,
--- 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);
--- 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
--- 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"} $
--- 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
--- 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
--- 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)
--- 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 =
--- 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, [])]]
--- 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])
--- 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
--- 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)))
--- 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))
--- 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
--- 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))
--- 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;
--- 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
--- 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
--- 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
--- 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
--- 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;
--- 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
--- 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
--- 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
--- 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) =
--- 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)
--- 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 =
--- 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 \
--- 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
--- 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 " "
--- 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
--- 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
--- 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
--- 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
--- 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..."
--- 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
--- 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
--- 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)
--- 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
--- 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))
--- 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
--- 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 =
--- 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 =>
--- 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};
--- 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
--- 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 =
--- 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
--- 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
--- 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
--- 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
--- 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))
--- 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
--- 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))
--- 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
--- 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
--- 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
--- 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)
--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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))
--- 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)
--- 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*)
--- 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;
--- 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;
--- 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)
--- 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;
--- 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')
--- 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 *)
--- 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';
--- 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
--- 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
--- 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))
--- 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}
--- 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;
--- 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 =
--- 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;
--- 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);
--- 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;
--- 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;
--- 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"
--- 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
--- 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
--- 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
--- 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 *)
--- 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)
--- 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
--- 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);
--- 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;
--- 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;
--- 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;
--- 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 *)
--- 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" []
--- 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;
--- 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);
--- 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
[] => ()
--- 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 *)
--- 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
--- 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}
--- 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
--- 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];
--- 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;
--- 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;
--- 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
--- 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));
--- 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);
--- 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
--- 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;
--- 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));
--- 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;
--- 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;