# HG changeset patch
# User wenzelm
# Date 1288862579 -3600
# Node ID 755862729f8d383020f6d759dc1bbc11e4cac253
# Parent  3e4bb6e7c3cae2fa4a923c38a2fd440f90844df4
tuned;

diff -r 3e4bb6e7c3ca -r 755862729f8d src/Pure/ML-Systems/timing.ML
--- 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