# HG changeset patch
# User wenzelm
# Date 1218738577 -7200
# Node ID 67d14d7c71431de008c4bf4fe9639ae6bb9cb75d
# Parent  1ba19c9edd18137b834dde41b4762d9008aaeeb3
tuned;

diff -r 1ba19c9edd18 -r 67d14d7c7143 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Aug 14 20:13:43 2008 +0200
+++ b/src/Pure/General/markup.ML	Thu Aug 14 20:29:37 2008 +0200
@@ -62,6 +62,7 @@
   val methodN: string val method: string -> T
   val ML_sourceN: string val ML_source: T
   val doc_sourceN: string val doc_source: T
+  val antiqN: string val antiq: 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
@@ -74,7 +75,6 @@
   val controlN: string val control: T
   val malformedN: string val malformed: T
   val tokenN: string val token: T
-  val antiqN: string val antiq: T
   val command_spanN: string val command_span: string -> T
   val ignored_spanN: string val ignored_span: T
   val malformed_spanN: string val malformed_span: T
@@ -202,6 +202,8 @@
 val (ML_sourceN, ML_source) = markup_elem "ML_source";
 val (doc_sourceN, doc_source) = markup_elem "doc_source";
 
+val (antiqN, antiq) = markup_elem "antiq";
+
 
 (* outer syntax *)
 
@@ -222,8 +224,6 @@
 
 val (tokenN, token) = markup_elem "token";
 
-val (antiqN, antiq) = markup_elem "antiq";
-
 val (command_spanN, command_span) = markup_string "command_span" nameN;
 val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
 val (malformed_spanN, malformed_span) = markup_elem "malformed_span";