# HG changeset patch
# User wenzelm
# Date 1218653842 -7200
# Node ID b67974f24d0c4b86f8f6c5b89516da9ac50771bd
# Parent  49503146b853f68b79c560f6259c81f97f51df91
tuned;

diff -r 49503146b853 -r b67974f24d0c src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Aug 13 20:57:20 2008 +0200
+++ b/src/Pure/General/markup.ML	Wed Aug 13 20:57:22 2008 +0200
@@ -64,7 +64,6 @@
   val command_declN: string val command_decl: string -> string -> T
   val keywordN: string val keyword: string -> T
   val commandN: string val command: string -> T
-  val tokenN: string val token: T
   val identN: string val ident: T
   val stringN: string val string: T
   val altstringN: string val altstring: T
@@ -72,6 +71,7 @@
   val commentN: string val comment: T
   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
@@ -204,7 +204,6 @@
 
 val (keywordN, keyword) = markup_string "keyword" nameN;
 val (commandN, command) = markup_string "command" nameN;
-val (tokenN, token) = markup_elem "token";
 val (identN, ident) = markup_elem "ident";
 val (stringN, string) = markup_elem "string";
 val (altstringN, altstring) = markup_elem "altstring";
@@ -213,6 +212,8 @@
 val (controlN, control) = markup_elem "control";
 val (malformedN, malformed) = markup_elem "malformed";
 
+val (tokenN, token) = markup_elem "token";
+
 val (antiqN, antiq) = markup_elem "antiq";
 
 val (command_spanN, command_span) = markup_string "command_span" nameN;