diff -r cd41e3903fbf -r eb65c9d17e2f src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Tue Nov 29 21:29:53 2011 +0100
+++ b/src/Pure/General/timing.scala	Tue Nov 29 21:50:00 2011 +0100
@@ -1,5 +1,4 @@
 /*  Title:      Pure/General/timing.scala
-    Module:     PIDE
     Author:     Makarius
 
 Basic support for time measurement.
@@ -8,25 +7,6 @@
 package isabelle
 
 
-object Time
-{
-  def seconds(s: Double): Time = new Time((s * 1000.0) round)
-  def ms(m: Long): Time = new Time(m)
-}
-
-class Time private(val ms: Long)
-{
-  def seconds: Double = ms / 1000.0
-
-  def min(t: Time): Time = if (ms < t.ms) this else t
-  def max(t: Time): Time = if (ms > t.ms) this else t
-
-  override def toString =
-    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
-  def message: String = toString + "s"
-}
-
-
 object Timing
 {
   def timeit[A](message: String)(e: => A) =