diff -r be5aa2c9c9ad -r 73a2f3fe0e8c src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Fri Apr 08 15:56:14 2022 +0200
+++ b/src/Pure/ML/ml_lex.scala	Fri Apr 08 16:26:48 2022 +0200
@@ -281,7 +281,8 @@
     val toks = new mutable.ListBuffer[Token]
     var ctxt = context
     while (!in.atEnd) {
-      Parsers.parse(Parsers.token_line(SML, ctxt), in) match {
+      val result = Parsers.parse(Parsers.token_line(SML, ctxt), in)
+      (result : @unchecked) match {
         case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest
         case Parsers.NoSuccess(_, rest) =>
           error("Unexpected failure of tokenizing input:\n" + rest.source.toString)