# HG changeset patch
# User wenzelm
# Date 1184879926 -7200
# Node ID b1861768d8f45fceddea2cdd741d154e494d8723
# Parent  72bb3494746fd6881c39638d5bdc5a8680f4da79
tuned;

diff -r 72bb3494746f -r b1861768d8f4 src/Pure/General/output.ML
--- 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*)