--- a/src/Pure/General/markup.ML Fri Aug 15 16:08:08 2008 +0200
+++ b/src/Pure/General/markup.ML Fri Aug 15 17:03:52 2008 +0200
@@ -65,6 +65,8 @@
val ML_sourceN: string val ML_source: T
val doc_sourceN: string val doc_source: T
val antiqN: string val antiq: T
+ val ML_antiqN: string val ML_antiq: string -> T
+ val doc_antiqN: string val doc_antiq: string -> T
val keyword_declN: string val keyword_decl: string -> T
val command_declN: string val command_decl: string -> string -> T
val keywordN: string val keyword: string -> T
@@ -209,6 +211,8 @@
val (doc_sourceN, doc_source) = markup_elem "doc_source";
val (antiqN, antiq) = markup_elem "antiq";
+val (ML_antiqN, ML_antiq) = markup_string "ML_antiq" nameN;
+val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN;
(* outer syntax *)