--- a/ProgTutorial/Recipes/TimeLimit.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Recipes/TimeLimit.thy	Thu May 16 19:56:12 2019 +0200
@@ -21,12 +21,12 @@
 
   Now the call 
 
-  @{ML_response_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"}
+  @{ML_matchresult_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
 
-@{ML_response_fake_both [display,gray]
+@{ML_matchresult_fake_both [display,gray]
 "Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) 
   handle TIMEOUT => ~1"
 "~1"}
@@ -40,7 +40,7 @@
 
 \begin{readmore}
    The function @{ML "apply" in Timeout} is defined in the structure
-  @{ML_struct Timeout} which can be found in the file 
+  @{ML_structure Timeout} which can be found in the file 
   @{ML_file "Pure/concurrent/timeout.ML"}.
 \end{readmore}