src/Pure/Tools/build_schedule.scala

         }
 
       def linear(p0: (Int, Time), p1: (Int, Time)): Time = {
         val a = (p1._2 - p0._2).scale(1.0 / (p1._1 - p0._1))
         val b = p0._2 - a.scale(p0._1)
-        Time.ms((a.scale(threads) + b).ms max 0)
+        (a.scale(threads) + b) max Time.zero
       }
 
       val mono_prefix = sorted_prefix(entries, e => -e._2.ms)
 
       val is_mono = entries == mono_prefix

             if m != n
           } yield (t0 - t1).scale(n.toDouble * m / (m - n)))
         val t_c =
           Timing_Data.median_time(for ((n, t) <- mono_prefix) yield t - t_p.scale(1.0 / n))
 
-        def model(threads: Int): Time = Time.ms((t_c + t_p.scale(1.0 / threads)).ms max 0)
+        def model(threads: Int): Time = (t_c + t_p.scale(1.0 / threads)) max Time.zero
 
         if (is_mono || in_prefix) model(threads)
         else {
           val post_inflection = entries.drop(mono_prefix.length).head
           val inflection_threads = inflection_point(mono_prefix.last._1, post_inflection._1)

           case None => node -> best_time(node)
           case Some(job) =>
             val estimate =
               timing_data.estimate(job.name, job.node_info.hostname,
                 host_infos.num_threads(job.node_info))
-            node -> Time.ms((Time.now() - job.start_date.time + estimate).ms max 0)
+            node -> ((Time.now() - job.start_date.time + estimate) max Time.zero)
         }
 
       val max_parallel = parallel_paths(state.ready.map(_.name).map(remaining_time))
       val next_sorted = state.next_ready.sortBy(max_time(_).ms).reverse