added convenience operation seconds: real -> time;

--- a/src/Pure/ML-Systems/timing.ML	Tue Nov 02 20:16:56 2010 +0100
+++ b/src/Pure/ML-Systems/timing.ML	Tue Nov 02 20:31:46 2010 +0100
@@ -1,9 +1,11 @@
 (*  Title:      Pure/ML-Systems/timing.ML
     Author:     Makarius
 
-Compiler-independent timing functions.
+Basic support for timing.
 *)
 
+fun seconds s = Time.fromNanoseconds (Real.ceil (s * 1E9));
+
 fun start_timing () =
   let
     val real_timer = Timer.startRealTimer ();