# HG changeset patch
# User wenzelm
# Date 1218812632 -7200
# Node ID a06f78f917e007619b8a3c29aaf76dbc041c8852
# Parent  7c97cf70d663ef8e284347cd46340103397d8b24
added ML_antiq, doc_antiq;

diff -r 7c97cf70d663 -r a06f78f917e0 src/Pure/General/markup.ML
--- 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 *)