--- 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)))));