src/Pure/General/timing.ML

--- a/src/Pure/General/timing.ML	Wed Jan 09 12:22:09 2013 +0100
+++ b/src/Pure/General/timing.ML	Wed Jan 09 13:38:57 2013 +0100
@@ -21,7 +21,6 @@
   val result: start -> timing
   val timing: ('a -> 'b) -> 'a -> timing * 'b
   val is_relevant: timing -> bool
-  val properties: timing -> Properties.T
   val message: timing -> string
 end
 
@@ -67,17 +66,6 @@
   in (result start, y) end;
 
 
-(* properties *)
-
-fun property name time =
-  [(name, Time.toString time)] handle Time.Time => [];
-
-fun properties {elapsed, cpu, gc} =
-  property "time_elapsed" elapsed @
-  property "time_cpu" cpu @
-  property "time_GC" gc;
-
-
 (* timing messages *)
 
 val min_time = Time.fromMilliseconds 1;