tuned;

--- a/src/Pure/General/output.ML	Thu Jul 19 23:18:45 2007 +0200
+++ b/src/Pure/General/output.ML	Thu Jul 19 23:18:46 2007 +0200
@@ -141,16 +141,16 @@
 (*global timing mode*)
 val timing = ref false;
 
-(*a conditional timing function: applies f to () and, if the flag is true,
-  prints its runtime on warning channel*)
+(*conditional timing*)
 fun cond_timeit flag f =
   if flag then
-    let val start = start_timing ()
-        val result = f ()
+    let
+      val start = start_timing ();
+      val result = f ();
     in warning (end_timing start); result end
   else f ();
 
-(*unconditional timing function*)
+(*unconditional timing*)
 fun timeit x = cond_timeit true x;
 
 (*timed application function*)