src/Pure/PIDE/document.scala

   object Node
   {
     sealed case class Header(
       imports: List[Name],
       keywords: Thy_Header.Keywords,
-      files: List[String],
       errors: List[String] = Nil)
     {
       def error(msg: String): Header = copy(errors = errors ::: List(msg))
     }
 
-    def bad_header(msg: String): Header = Header(Nil, Nil, Nil, List(msg))
+    def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
 
     object Name
     {
       val empty = Name("", "", "")