src/Pure/Concurrent/future.ML

--- a/src/Pure/Concurrent/future.ML	Tue Nov 02 20:31:46 2010 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Nov 02 20:55:12 2010 +0100
@@ -253,7 +253,7 @@
 val status_ticks = Unsynchronized.ref 0;
 
 val last_round = Unsynchronized.ref Time.zeroTime;
-val next_round = Time.fromMilliseconds 50;
+val next_round = seconds 0.05;
 
 fun scheduler_next () = (*requires SYNCHRONIZED*)
   let