diff -r 3e30ea95c7aa -r 009ca4807baa CookBook/Recipes/TimeLimit.thy
--- a/CookBook/Recipes/TimeLimit.thy	Wed Mar 11 17:38:17 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Wed Mar 11 22:34:49 2009 +0000
@@ -11,16 +11,13 @@
   {\bf Solution:} This can be achieved using the function 
   @{ML timeLimit in TimeLimit}.\smallskip
 
-  Assume you defined the Ackermann function:
-
-  *}
+  Assume you defined the Ackermann function on the ML-level.
+*}
 
 ML{*fun ackermann (0, n) = n + 1
   | ackermann (m, 0) = ackermann (m - 1, 1)
   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
 
-ML {* ackermann (3,4) *} 
-
 text {*
 
   Now the call 
@@ -28,7 +25,7 @@
   @{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:
+  in a time limit of five seconds. For this you have to write
 
 @{ML_response [display,gray]
 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 
@@ -39,7 +36,7 @@
   is reached.
 
   Note that @{ML  "timeLimit" in TimeLimit} is only meaningful when you use PolyML, 
-  because PolyML has a rich infrastructure for multithreading programming on 
+  because PolyML has the infrastructure for multithreading programming on 
   which @{ML "timeLimit" in TimeLimit} relies.
 
 \begin{readmore}
@@ -50,5 +47,4 @@
 
  
 *}
-
 end
\ No newline at end of file