src/Pure/Tools/build_job.scala

           case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
         }
 
       val result = {
         val theory_timing =
-          theory_timings.iterator.map(
+          theory_timings.iterator.flatMap(
             {
-              case props @ Markup.Name(name) => name -> props
-              case _ => ???
+              case props @ Markup.Name(name) => Some(name -> props)
+              case _ => None
             }).toMap
         val used_theory_timings =
           for { (name, _) <- deps(session_name).used_theories }
             yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))