diff -r a1363da718aa -r b13ab7d11b90 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Apr 04 22:42:12 2022 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Apr 04 23:33:14 2022 +0200
@@ -123,7 +123,7 @@
 
   /* parser */
 
-  trait Parser extends Parse.Parser {
+  trait Parsers extends Parse.Parsers {
     val header: Parser[Thy_Header] = {
       val load_command =
         ($$$("(") ~! (position(name) <~ $$$(")")) ^^ { case _ ~ x => x }) |
@@ -199,7 +199,7 @@
     (drop_tokens, tokens1 ::: tokens2)
   }
 
-  private object Parser extends Parser {
+  private object Parsers extends Parsers {
     def parse_header(tokens: List[Token], pos: Token.Pos): Thy_Header =
       parse(commit(header), Token.reader(tokens, pos)) match {
         case Success(result, _) => result
@@ -219,7 +219,7 @@
       if (command) Token.Pos.command
       else skip_tokens.foldLeft(Token.Pos.file(node_name.node))(_ advance _)
 
-    Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
+    Parsers.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
   }
 }