diff -r 15f001295a7b -r 5c16895d548b src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -222,8 +222,8 @@
 
 val scan_chr =
   $$ "\\" |-- Scan.one Symbol.not_eof ||
-  Scan.one (not_equal "'" andf Symbol.not_eof) ||
-  $$ "'" --| Scan.ahead (Scan.one (not_equal "'"));
+  Scan.one (fn s => s <> "'" andalso Symbol.not_eof s) ||
+  $$ "'" --| Scan.ahead (~$$ "'");
 
 val scan_str =
   $$ "'" |-- $$ "'" |-- !! (lex_err "missing end of string" "''")
@@ -243,8 +243,8 @@
 val scan_cmt =
   Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) ||
   Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) ||
-  Scan.lift ($$ "*" --| Scan.ahead (Scan.one (not_equal ")"))) ||
-  Scan.lift (Scan.one (not_equal "*" andf Symbol.not_eof));
+  Scan.lift ($$ "*" --| Scan.ahead (~$$ ")")) ||
+  Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.not_eof s));
 
 val scan_comment =
   $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")