--- a/ProgTutorial/Recipes/TimeLimit.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/TimeLimit.thy	Tue May 14 11:10:53 2019 +0200
@@ -3,13 +3,12 @@
 begin
 
 section {* Restricting the Runtime of a Function\label{rec:timeout} *} 
-
 text {*
   {\bf Problem:}
   Your tool should run only a specified amount of time.\smallskip
 
-  {\bf Solution:} In PolyML 5.2.1 and later, this can be achieved 
-  using the function @{ML timeLimit in TimeLimit}.\smallskip
+  {\bf Solution:} In Isabelle 2016-1 and later, this can be achieved 
+  using the function @{ML apply in Timeout}.\smallskip
 
   Assume you defined the Ackermann function on the ML-level.
 *}
@@ -28,21 +27,21 @@
   in a time limit of five seconds. For this you have to write
 
 @{ML_response_fake_both [display,gray]
-"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) 
-  handle TimeLimit.TimeOut => ~1"
+"Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) 
+  handle TIMEOUT => ~1"
 "~1"}
 
   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 5.2.1
+  Note that @{ML  "apply" in Timeout} 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.
+  programming on which @{ML "apply" in Timeout} relies.
 
 \begin{readmore}
-   The function @{ML "timeLimit" in TimeLimit} is defined in the structure
-  @{ML_struct TimeLimit} which can be found in the file 
-  @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}.
+   The function @{ML "apply" in Timeout} is defined in the structure
+  @{ML_struct Timeout} which can be found in the file 
+  @{ML_file "Pure/concurrent/timeout.ML"}.
 \end{readmore}