diff -r 043ef82000b4 -r 371e4375c994 CookBook/Recipes/TimeLimit.thy
--- a/CookBook/Recipes/TimeLimit.thy	Wed Mar 18 03:27:15 2009 +0100
+++ b/CookBook/Recipes/TimeLimit.thy	Wed Mar 18 18:27:48 2009 +0100
@@ -27,7 +27,7 @@
   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,gray]
+@{ML_response_fake_both [display,gray]
 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 
   handle TimeLimit.TimeOut => ~1"
 "~1"}
@@ -35,9 +35,9 @@
   where @{text TimeOut} is the exception raised when the time limit
   is reached.
 
-  Note that @{ML  "timeLimit" in TimeLimit} is only meaningful when you use PolyML, 
-  because PolyML has the infrastructure for multithreaded programming on 
-  which @{ML "timeLimit" in TimeLimit} relies.
+  Note that @{ML  "timeLimit" in TimeLimit} is only meaningful when you use PolyML 5.2.1
+  or later, because this version of PolyML has the infrastructure for multithreaded 
+  programming on which @{ML "timeLimit" in TimeLimit} relies.
 
 \begin{readmore}
    The function @{ML "timeLimit" in TimeLimit} is defined in the structure