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