src/Tools/WWW_Find/unicode_symbols.ML

--- a/src/Tools/WWW_Find/unicode_symbols.ML	Wed May 05 09:24:42 2010 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Wed May 05 18:25:34 2010 +0200
@@ -82,7 +82,7 @@
   -- Scan.many (not o Symbol.is_ascii_blank o symbol)
   >> (token AsciiSymbol o op ::);
 
-fun not_contains xs c = not ((symbol c) mem_string (explode xs));
+fun not_contains xs c = not (member (op =) (explode xs) (symbol c));
 val scan_comment =
   $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
   >> token Comment;