diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Recipes/TimeLimit.thy
--- a/CookBook/Recipes/TimeLimit.thy	Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Wed Jan 14 23:44:14 2009 +0000
@@ -23,12 +23,12 @@
 
   Now the call 
 
-  @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"}
+  @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"}
 
   takes a bit of time before it finishes. To avoid this, the call can be encapsulated 
   in a time limit of five seconds. For this you have to write:
 
-@{ML_response [display]
+@{ML_response [display,gray]
 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 
   handle TimeOut => ~1"
 "~1"}