--- a/src/Pure/Isar/token.ML Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Isar/token.ML Tue Nov 11 18:16:25 2014 +0100
@@ -268,8 +268,8 @@
val tree = XML.Elem (Markup.token delimited (Position.properties_of pos), [XML.Text source]);
in YXML.string_of tree end;
-fun source_position_of (Token ((source, (pos, _)), (kind, _), _)) =
- {delimited = delimited_kind kind, text = source, pos = pos};
+fun source_position_of (Token ((source, range), (kind, _), _)) =
+ {delimited = delimited_kind kind, text = source, range = range};
fun content_of (Token (_, (_, x), _)) = x;