src/Pure/General/value.scala

       unapply(s) getOrElse error("Bad real: " + quote(s))
   }
 
   object Seconds
   {
-    def apply(x: Time): java.lang.String = x.toString
+    def apply(t: Time): java.lang.String =
+    {
+      val s = t.seconds
+      if (s.toInt.toDouble == s) s.toInt.toString else t.toString
+    }
     def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
     def parse(s: java.lang.String): Time =
       unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
   }
 }