tuned;

--- a/src/Pure/ML-Systems/timing.ML	Wed Nov 03 21:53:56 2010 +0100
+++ b/src/Pure/ML-Systems/timing.ML	Thu Nov 04 10:22:59 2010 +0100
@@ -1,10 +1,10 @@
 (*  Title:      Pure/ML-Systems/timing.ML
     Author:     Makarius
 
-Basic support for timing.
+Basic support for time measurement.
 *)
 
-fun seconds s = Time.fromNanoseconds (Real.ceil (s * 1E9));
+val seconds = Time.fromReal;
 
 fun start_timing () =
   let