src/Pure/General/timing.scala

     else body
   }
 
   def factor_format(f: Double): String =
     String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
+
+  def merge(args: IterableOnce[Timing]): Timing =
+    args.iterator.foldLeft(zero)(_ + _)
 }
 
 sealed case class Timing(elapsed: Time, cpu: Time, gc: Time) {
   def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
   def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant