--- a/src/Pure/ML/ml_context.ML Wed Mar 12 21:58:48 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Wed Mar 12 22:41:04 2014 +0100
@@ -23,6 +23,7 @@
val get_stored_thm: unit -> thm
val ml_store_thms: string * thm list -> unit
val ml_store_thm: string * thm -> unit
+ val check_antiquotation: Proof.context -> xstring * Position.T -> string
val print_antiquotations: Proof.context -> unit
type decl = Proof.context -> string * string
val antiquotation: binding -> 'a context_parser ->
@@ -109,6 +110,9 @@
val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
+fun check_antiquotation ctxt =
+ #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt);
+
fun add_antiquotation name f thy = thy
|> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);