src/Tools/WWW_Find/unicode_symbols.ML
changeset 36692 54b64d4ad524
parent 33823 24090eae50b6
child 36960 01594f816e3a
     1.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4    -- Scan.many (not o Symbol.is_ascii_blank o symbol)
     1.5    >> (token AsciiSymbol o op ::);
     1.6  
     1.7 -fun not_contains xs c = not ((symbol c) mem_string (explode xs));
     1.8 +fun not_contains xs c = not (member (op =) (explode xs) (symbol c));
     1.9  val scan_comment =
    1.10    $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
    1.11    >> token Comment;