diff -r 803431dcc7fb -r e3ac771235f7 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Sep 07 13:16:45 2010 +0200
+++ b/src/Pure/General/markup.ML	Tue Sep 07 14:08:21 2010 +0200
@@ -58,6 +58,7 @@
   val literalN: string val literal: T
   val inner_stringN: string val inner_string: T
   val inner_commentN: string val inner_comment: T
+  val token_rangeN: string val token_range: T
   val sortN: string val sort: T
   val typN: string val typ: T
   val termN: string val term: T
@@ -239,6 +240,8 @@
 val (inner_stringN, inner_string) = markup_elem "inner_string";
 val (inner_commentN, inner_comment) = markup_elem "inner_comment";
 
+val (token_rangeN, token_range) = markup_elem "token_range";
+
 val (sortN, sort) = markup_elem "sort";
 val (typN, typ) = markup_elem "typ";
 val (termN, term) = markup_elem "term";