diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/check_keywords.scala
--- a/src/Pure/Tools/check_keywords.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/check_keywords.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -22,7 +22,7 @@
 
       val result =
         parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
-          case Success(res, _) => for (Some(x) <- res) yield x
+          case Success(res, _) => for (case Some(x) <- res) yield x
           case bad => error(bad.toString)
         }
     }