src/Pure/Thy/thy_syntax.scala

       node_name: Document.Node.Name,
       span: List[Token],
       doc_blobs: Document.Blobs)
     : List[Command.Blob] =
   {
-    span_files(syntax, span).map(file =>
+    span_files(syntax, span).map(file_name =>
       Exn.capture {
         val name =
-          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
-        (name, doc_blobs.get(name).map(_.sha1_digest))
+          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file_name)))
+        val blob =
+          doc_blobs.get(name) match {
+            case Some((bytes, file)) => Some((bytes.sha1_digest, file))
+            case None => None
+          }
+        (name, blob)
       }
     )
   }