--- a/ProgTutorial/Recipes/ExternalSolver.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Tue May 21 14:37:39 2019 +0200
@@ -27,7 +27,7 @@
   properly. For example, the following expression takes only approximately
   one second:
 
-  @{ML_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
     \<open>Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output "sleep 30"
      handle TIMEOUT => ("timeout", ~1)\<close> \<open>("timeout", ~1)\<close>}
 
@@ -46,7 +46,7 @@
 
   In Isabelle, this application may now be executed by
 
-  @{ML_matchresult_fake [display,gray] \<open>Isabelle_System.bash_output "$FOO"\<close> \<open>\<dots>\<close>}
+  @{ML_response [display,gray] \<open>Isabelle_System.bash_output "$FOO"\<close> \<open>\<dots>\<close>}
 \<close>