doc-src/antiquote_setup.ML
changeset 43563 aeabb735883a
parent 42666 fee67c099d03
child 43564 9864182c6bad
     1.1 --- a/doc-src/antiquote_setup.ML	Mon Jun 27 17:20:24 2011 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon Jun 27 17:51:28 2011 +0200
     1.3 @@ -192,7 +192,9 @@
     1.4  val _ = entity_antiqs no_check "isatt" "executable";
     1.5  val _ = entity_antiqs (K check_tool) "isatt" "tool";
     1.6  val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
     1.7 -val _ = entity_antiqs no_check "" "ML antiquotation";  (* FIXME proper check *)
     1.8 +val _ =
     1.9 +  entity_antiqs
    1.10 +    (thy_check ML_Context.intern_antiq ML_Context.defined_antiq) "" Markup.ML_antiquotationN;
    1.11  
    1.12  end;
    1.13