src/Pure/Thy/thy_syntax.scala

--- a/src/Pure/Thy/thy_syntax.scala	Thu Feb 27 12:48:59 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Feb 27 14:07:04 2014 +0100
@@ -268,14 +268,9 @@
       Exn.capture {
         val name =
           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
-          }
+        val blob = doc_blobs.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
         (name, blob)
-      }
-    )
+      })
   }