src/Pure/Isar/outer_lex.ML

--- a/src/Pure/Isar/outer_lex.ML	Thu Sep 21 19:04:12 2006 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Thu Sep 21 19:04:20 2006 +0200
@@ -190,8 +190,7 @@
 
 (* scan symbolic idents *)
 
-val sym_chars = explode "!#$%&*+-/<=>?@^_|~";
-fun is_sym_char s = s mem sym_chars;
+val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
 
 val scan_symid =
   Scan.any1 is_sym_char >> implode ||