src/Pure/library.ML

--- a/src/Pure/library.ML	Fri Nov 28 10:54:13 1997 +0100
+++ b/src/Pure/library.ML	Fri Nov 28 10:59:14 1997 +0100
@@ -802,6 +802,17 @@
 
 (** timing **)
 
+(*a conditional timing function: applies f to () and, if the flag is true,
+  prints its runtime*)
+fun cond_timeit flag f =
+  if flag then
+    let val start = startTiming()
+        val result = f ()
+    in
+	writeln (endTiming start);  result
+    end
+  else f ();
+
 (*unconditional timing function*)
 fun timeit x = cond_timeit true x;