src/Pure/Thy/thy_syntax.scala

     {
       /* stack operations */
 
       def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
       var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
-        List((0, node_name.theory, buffer()))
+        List((0, node_name.toString, buffer()))
 
       @tailrec def close(level: Int => Boolean)
       {
         stack match {
           case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>

       span: List[Token]): Command.Blobs =
   {
     val files = span_files(syntax, span)
     files.map(file => {
       // FIXME proper thy_load append
-      val file_name = Document.Node.Name(name.dir + file, name.dir, "")
+      val file_name = Document.Node.Name(name.master_dir + file)
       (file_name, all_blobs.get(file_name).map(_.sha1_digest))
     })
   }