diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Recipes/TimeLimit.thy
--- a/CookBook/Recipes/TimeLimit.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -11,7 +11,7 @@
   {\bf Solution:} This can be achieved using the function 
   @{ML timeLimit in TimeLimit}.\smallskip
 
-  Assume the following infamous function:
+  Assume you defined the Ackermann function:
 
   *}
 
@@ -27,7 +27,7 @@
 
   @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"}
 
-  takes a bit of time to finish. To avoid this, the call can be encapsulated 
+  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]