--- 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";