--- a/NEWS Sat Aug 17 13:39:28 2019 +0200
+++ b/NEWS Sat Aug 17 17:21:30 2019 +0200
@@ -57,6 +57,8 @@
Theory.join_theory recovers a single result theory. See also the example
in theory "HOL-ex.Join_Theory".
+* Antiquotation @{oracle_name} inlines a formally checked oracle name.
+
New in Isabelle2019 (June 2019)
--- a/etc/symbols Sat Aug 17 13:39:28 2019 +0200
+++ b/etc/symbols Sat Aug 17 17:21:30 2019 +0200
@@ -429,6 +429,7 @@
\<^type_abbrev> argument: cartouche
\<^type_name> argument: cartouche
\<^type_syntax> argument: cartouche
+\<^oracle_name> argument: cartouche
\<^code> argument: cartouche
\<^computation> argument: cartouche
\<^computation_conv> argument: cartouche
--- a/src/HOL/ex/Iff_Oracle.thy Sat Aug 17 13:39:28 2019 +0200
+++ b/src/HOL/ex/Iff_Oracle.thy Sat Aug 17 17:21:30 2019 +0200
@@ -36,8 +36,7 @@
ML \<open>iff_oracle (\<^theory>, 10)\<close>
ML \<open>
- Thm.peek_status (iff_oracle (\<^theory>, 10));
- \<^assert> (#oracle it);
+ \<^assert> (map #1 (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
\<close>
text \<open>These oracle calls had better fail.\<close>
--- a/src/Pure/ML/ml_antiquotations.ML Sat Aug 17 13:39:28 2019 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Sat Aug 17 17:21:30 2019 +0200
@@ -78,6 +78,10 @@
ML_Antiquotation.value_embedded \<^binding>\<open>cprop\<close> (Args.prop >> (fn t =>
"Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>oracle_name\<close>
+ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
+ ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos)))) #>
+
ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
(Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
--- a/src/Pure/thm.ML Sat Aug 17 13:39:28 2019 +0200
+++ b/src/Pure/thm.ML Sat Aug 17 17:21:30 2019 +0200
@@ -127,6 +127,7 @@
val oracle_space: theory -> Name_Space.T
val pretty_oracle: Proof.context -> string -> Pretty.T
val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list
+ val check_oracle: Proof.context -> xstring * Position.T -> string
(*inference rules*)
val assume: cterm -> thm
val implies_intr: cterm -> thm -> thm
@@ -1069,6 +1070,9 @@
fun extern_oracles verbose ctxt =
map #1 (Name_Space.markup_table verbose ctxt (get_oracles (Proof_Context.theory_of ctxt)));
+fun check_oracle ctxt =
+ Name_Space.check (Context.Proof ctxt) (get_oracles (Proof_Context.theory_of ctxt)) #> #1;
+
(*** Meta rules ***)