ML_Context.check_antiquotation still required;

--- a/src/Doc/antiquote_setup.ML	Wed Mar 12 21:58:48 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Wed Mar 12 22:41:04 2014 +0100
@@ -267,7 +267,7 @@
     entity_antiqs no_check "" "inference" #>
     entity_antiqs no_check "isatt" "executable" #>
     entity_antiqs (K check_tool) "isatool" "tool" #>
-    entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN #>
+    entity_antiqs (can o ML_Context.check_antiquotation) "" Markup.ML_antiquotationN #>
     entity_antiqs (K (is_action o #1)) "isatt" "action");
 
 end;

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