--- a/src/Tools/WWW_Find/unicode_symbols.ML Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Sat Nov 20 00:53:26 2010 +0100
@@ -82,7 +82,7 @@
-- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
>> (token AsciiSymbol o op ::);
-fun not_contains xs c = not (member (op =) (explode xs) (Symbol_Pos.symbol c));
+fun not_contains xs c = not (member (op =) (raw_explode xs) (Symbol_Pos.symbol c));
val scan_comment =
$$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
>> token Comment;