--- a/src/Pure/Isar/token.ML Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/Isar/token.ML Sun Jul 10 20:59:04 2011 +0200
@@ -180,8 +180,9 @@
(* token content *)
-fun source_of (Token ((source, (pos, _)), _, _)) =
- YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
+fun source_of (Token ((source, (pos, _)), (_, x), _)) =
+ if YXML.detect x then x
+ else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);