src/Tools/WWW_Find/unicode_symbols.ML
changeset 40627 becf5d5187cc
parent 40527 e0c000e40c05
child 43469 882108e9536a
--- 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;