diff -r 77ef8bef0593 -r 894f29abe5fc src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Mar 04 21:04:27 2021 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Mar 04 21:19:05 2021 +0100
@@ -186,10 +186,10 @@
   private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) =
   {
     val token = Token.Parsers.token(bootstrap_keywords)
-    def make_tokens(in: Reader[Char]): Stream[Token] =
+    def make_tokens(in: Reader[Char]): LazyList[Token] =
       token(in) match {
         case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
-        case _ => Stream.empty
+        case _ => LazyList.empty
       }
 
     val all_tokens = make_tokens(reader)