# HG changeset patch
# User wenzelm
# Date 1566055290 -7200
# Node ID d0b75c59beca26697ec4fb39553c8c72c975ee6b
# Parent  2c7c8be65b7d0c5faaa1b088881603fb8b063c86
added ML antiquotation @{oracle_name};

diff -r 2c7c8be65b7d -r d0b75c59beca NEWS
--- 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)
diff -r 2c7c8be65b7d -r d0b75c59beca etc/symbols
--- 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
diff -r 2c7c8be65b7d -r d0b75c59beca src/HOL/ex/Iff_Oracle.thy
--- 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>
diff -r 2c7c8be65b7d -r d0b75c59beca src/Pure/ML/ml_antiquotations.ML
--- 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)))));
diff -r 2c7c8be65b7d -r d0b75c59beca src/Pure/thm.ML
--- 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 ***)