src/Tools/WWW_Find/unicode_symbols.ML

--- a/src/Tools/WWW_Find/unicode_symbols.ML	Mon Jun 20 23:19:38 2011 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Mon Jun 20 23:21:24 2011 +0200
@@ -88,11 +88,10 @@
   >> token Comment;
 
 fun is_sym s =
-  Symbol.not_eof s andalso
-    (case Symbol.decode s of
-      Symbol.Sym _ => true
-    | Symbol.Ctrl _ => true
-    | _ => false);
+  (case Symbol.decode s of
+    Symbol.Sym _ => true
+  | Symbol.Ctrl _ => true
+  | _ => false);
 
 fun tokenize syms =
   let