# HG changeset patch
# User wenzelm
# Date 1394660464 -3600
# Node ID 1bc0bea908c396ca321ca3c06814194879d53437
# Parent  451d5b73f8cf1a58d64d8b20956b10a21aa73360
ML_Context.check_antiquotation still required;

diff -r 451d5b73f8cf -r 1bc0bea908c3 src/Doc/antiquote_setup.ML
--- 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;
diff -r 451d5b73f8cf -r 1bc0bea908c3 src/Pure/ML/ml_context.ML
--- 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);