diff -r 0385292321a0 -r 5199ee17c7d7 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Sun Sep 04 15:21:50 2011 +0200
+++ b/src/Pure/General/timing.scala	Sun Sep 04 15:49:59 2011 +0200
@@ -9,6 +9,7 @@
 object Time
 {
   def seconds(s: Double): Time = new Time((s * 1000.0) round)
+  def ms(m: Long): Time = new Time(m)
 }
 
 class Time(val ms: Long)