diff -r 29787dcf7b2e -r b63c72776f03 ProgTutorial/Recipes/Timing.thy
--- a/ProgTutorial/Recipes/Timing.thy	Mon Apr 13 08:30:48 2009 +0000
+++ b/ProgTutorial/Recipes/Timing.thy	Wed Apr 15 13:11:08 2009 +0000
@@ -33,7 +33,7 @@
   val res = tac st;
   val t_end = end_timing t_start;
 in
-  (warning (#message t_end); res)
+  (writeln (#message t_end); res)
 end*}
 
 text {*