src/Pure/Syntax/lexicon.ML

 fun lex_err msg prfx (cs, _) =
   "Inner lexical error: " ^ msg ^ " at " ^ quote (prfx ^ Symbol.beginning 10 cs);
 
 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" "''")
     (Scan.repeat scan_chr --| $$ "'" --| $$ "'");
 

 (* nested comments *)
 
 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" "(*")
     (Scan.pass 0 (Scan.repeat scan_cmt) -- $$ "*" -- $$ ")")
   >> K ();