src/Pure/General/time.scala

 
   def print_seconds(s: Double): String =
     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
 }
 
-final class Time private(val ms: Long)
+final class Time private(val ms: Long) extends AnyVal
 {
   def + (t: Time): Time = new Time(ms + t.ms)
 
   def seconds: Double = ms / 1000.0
 

   def max(t: Time): Time = if (ms > t.ms) this else t
 
   def is_zero: Boolean = ms == 0
   def is_relevant: Boolean = ms >= 1
 
-  override def hashCode: Int = ms.hashCode
-  override def equals(that: Any): Boolean =
-    that match {
-      case other: Time => ms == other.ms
-      case _ => false
-    }
-
   override def toString = Time.print_seconds(seconds)
 
   def message: String = toString + "s"
 }