--- a/ProgTutorial/Recipes/ExternalSolver.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Thu May 16 19:56:12 2019 +0200
@@ -19,7 +19,7 @@
 
   For example, consider running an ordinary shell commands:
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
     "Isabelle_System.bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
 
   Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
@@ -27,7 +27,7 @@
   properly. For example, the following expression takes only approximately
   one second:
 
-  @{ML_response_fake [display,gray] 
+  @{ML_matchresult_fake [display,gray] 
     "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
      handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
 
@@ -46,7 +46,7 @@
 
   In Isabelle, this application may now be executed by
 
-  @{ML_response_fake [display,gray] "Isabelle_System.bash_output \"$FOO\"" "\<dots>"}
+  @{ML_matchresult_fake [display,gray] "Isabelle_System.bash_output \"$FOO\"" "\<dots>"}
 \<close>