src/Pure/PIDE/document.scala

 
     val no_header = bad_header("No theory header")
 
     object Name
     {
-      val empty = Name("", "", "")
+      val empty = Name("")
 
       object Ordering extends scala.math.Ordering[Name]
       {
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
       }
     }
 
-    sealed case class Name(node: String, dir: String, theory: String)
+    sealed case class Name(node: String, master_dir: String = "", theory: String = "")
     {
       override def hashCode: Int = node.hashCode
       override def equals(that: Any): Boolean =
         that match {
           case other: Name => node == other.node