diff -r 210aabe359ab -r 10d719dbb3ee src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 18:07:10 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 18:30:56 2016 +0200
@@ -243,8 +243,8 @@
     chapter: String,
     groups: List[String],
     threads: Option[Int],
-    timing: Option[Timing],
-    ml_timing: Option[Timing],
+    timing: Timing,
+    ml_timing: Timing,
     status: Session_Status.Value)
   {
     def finished: Boolean = status == Session_Status.FINISHED
@@ -255,17 +255,15 @@
     def session(name: String): Session_Entry = sessions(name)
     def get_session(name: String): Option[Session_Entry] = sessions.get(name)
 
-    def finished(name: String): Boolean =
+    def get_default[A](name: String, f: Session_Entry => A, x: A): A =
       get_session(name) match {
-        case Some(entry) => entry.finished
-        case None => false
+        case Some(entry) => f(entry)
+        case None => x
       }
 
-    def timing(name: String): Timing =
-      (for (entry <- get_session(name); t <- entry.timing) yield t) getOrElse Timing.zero
-
-    def ml_timing(name: String): Timing =
-      (for (entry <- get_session(name); t <- entry.ml_timing) yield t) getOrElse Timing.zero
+    def finished(name: String): Boolean = get_default(name, _.finished, false)
+    def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
+    def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
   }
 
   private def parse_build_info(log_file: Log_File): Build_Info =
@@ -350,8 +348,8 @@
               chapter.getOrElse(name, ""),
               groups.getOrElse(name, Nil),
               threads.get(name),
-              timing.get(name),
-              ml_timing.get(name),
+              timing.getOrElse(name, Timing.zero),
+              ml_timing.getOrElse(name, Timing.zero),
               status)
           (name -> entry)
         }):_*)