diff -r d86540f6ea0d -r becf5d5187cc src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/Isar/token.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -265,7 +265,7 @@
 
 (* scan symbolic idents *)
 
-val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
+val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
 
 val scan_symid =
   Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||