diff -r 7104394df99a -r 77ea79aed99d src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue May 11 10:49:58 2004 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue May 11 14:00:02 2004 +0200
@@ -270,10 +270,10 @@
   Scan.lift ($$ "*" --| Scan.ahead (Scan.one (not_equal ")"))) ||
   Scan.lift (Scan.one (not_equal "*" andf Symbol.not_eof));
 
-val scan_comment =
-  $$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
+fun scan_comment xs =
+  ($$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*")
     (Scan.pass 0 (Scan.repeat scan_cmt) -- $$ "*" -- $$ ")")
-  >> K None;
+   >> K None) xs;