class Time as abstract datatype;

--- a/src/Pure/General/timing.scala	Sat Oct 22 23:28:24 2011 +0200
+++ b/src/Pure/General/timing.scala	Sat Oct 22 23:29:11 2011 +0200
@@ -12,7 +12,7 @@
   def ms(m: Long): Time = new Time(m)
 }
 
-class Time(val ms: Long)
+class Time private(val ms: Long)
 {
   def seconds: Double = ms / 1000.0
 

--- a/src/Pure/library.scala	Sat Oct 22 23:28:24 2011 +0200
+++ b/src/Pure/library.scala	Sat Oct 22 23:29:11 2011 +0200
@@ -219,7 +219,7 @@
     val stop = System.currentTimeMillis()
     System.err.println(
       (if (message == null || message.isEmpty) "" else message + ": ") +
-        new Time(stop - start).message + " elapsed time")
+        Time.ms(stop - start).message + " elapsed time")
     Exn.release(result)
   }
 }