src/Pure/Thy/thy_syntax.scala

--- a/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 21:49:31 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 22:12:54 2013 +0100
@@ -263,10 +263,7 @@
       Exn.capture {
         val name =
           Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
-        doc_blobs.get(name) match {
-          case Some(blob) => (name, blob.sha1_digest)
-          case None => error("No such file: " + quote(name.toString))
-        }
+        (name, doc_blobs.get(name).map(_.sha1_digest))
       }
     )
   }