src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:23:18 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:33:19 2020 +0100
@@ -213,7 +213,9 @@
       }
   }
 
-  def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
+  def read(reader: Reader[Char],
+    start: Token.Pos = Token.Pos.none,
+    strict: Boolean = true): Thy_Header =
   {
     val (_, tokens0) = read_tokens(reader, true)
     val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))