--- a/ProgTutorial/Recipes/TimeLimit.thy	Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/Recipes/TimeLimit.thy	Tue Jul 08 11:34:10 2014 +0100
@@ -22,7 +22,7 @@
 
   Now the call 
 
-  @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"}
+  @{ML_response_fake_both [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