diff -r 6103b0eadbf2 -r f7c97e64cc2a ProgTutorial/Readme.thy
--- a/ProgTutorial/Readme.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Readme.thy	Thu May 16 19:56:12 2019 +0200
@@ -54,7 +54,7 @@
   \end{tabular}
   \end{center}
 
-  \item[$\bullet$] \<open>@{ML_response "expr" "pat"}\<close> should be used to
+  \item[$\bullet$] \<open>@{ML_matchresult "expr" "pat"}\<close> should be used to
   display ML-expressions and their response.  The first expression is checked
   like in the antiquotation \<open>@{ML "expr"}\<close>; the second is a pattern
   that specifies the result the first expression produces. This pattern can
@@ -63,8 +63,8 @@
 
   \begin{center}\small
   \begin{tabular}{l}
-  \<open>@{ML_response "1+2" "3"}\<close>\\
-  \<open>@{ML_response "(1+2,3)" "(3,\<dots>)"}\<close>
+  \<open>@{ML_matchresult "1+2" "3"}\<close>\\
+  \<open>@{ML_matchresult "(1+2,3)" "(3,\<dots>)"}\<close>
   \end{tabular}
   \end{center}
 
@@ -72,8 +72,8 @@
 
   \begin{center}\small
   \begin{tabular}{p{3cm}p{3cm}}
-  @{ML_response "1+2" "3"} &  
-  @{ML_response "(1+2,3)" "(3,\<dots>)"}
+  @{ML_matchresult "1+2" "3"} &  
+  @{ML_matchresult "(1+2,3)" "(3,\<dots>)"}
   \end{tabular}
   \end{center}
   
@@ -81,17 +81,17 @@
   constructed: it does not work when the code produces an exception or returns 
   an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
 
-  \item[$\bullet$] \<open>@{ML_response_fake "expr" "pat"}\<close> works just
-  like the antiquotation \<open>@{ML_response "expr" "pat"}\<close> above,
+  \item[$\bullet$] \<open>@{ML_matchresult_fake "expr" "pat"}\<close> works just
+  like the antiquotation \<open>@{ML_matchresult "expr" "pat"}\<close> above,
   except that the result-specification is not checked. Use this antiquotation
   when the result cannot be constructed or the code generates an
   exception. Examples are:
 
   \begin{center}\small
   \begin{tabular}{ll}
-  \<open>@{ML_response_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\
+  \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\
                                & \<open>"a + b = c"}\<close>\smallskip\\ 
-  \<open>@{ML_response_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ 
+  \<open>@{ML_matchresult_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ 
                                & \<open>"Exception FAIL raised"}\<close>
   \end{tabular}
   \end{center}
@@ -100,21 +100,21 @@
 
   \begin{center}\small
   \begin{tabular}{p{7.2cm}}
-  @{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\
-  @{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}
+  @{ML_matchresult_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\
+  @{ML_matchresult_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}
   \end{tabular}
   \end{center}
   
   This output mimics to some extend what the user sees when running the
   code.
 
-  \item[$\bullet$] \<open>@{ML_response_fake_both "expr" "pat"}\<close> can be
+  \item[$\bullet$] \<open>@{ML_matchresult_fake_both "expr" "pat"}\<close> can be
   used to show erroneous code. Neither the code nor the response will be
   checked. An example is:
 
   \begin{center}\small
   \begin{tabular}{ll}
-  \<open>@{ML_response_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\
+  \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\
                                     & \<open>"Type unification failed \<dots>"}\<close>
   \end{tabular}
   \end{center}