--- a/ProgTutorial/Solutions.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Solutions.thy	Tue May 21 14:37:39 2019 +0200
@@ -55,7 +55,7 @@
   \<open>-1\<close> to account for the deleted quantifier. An example is 
   as follows:
 
-  @{ML_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>@{prop "\<forall>x y z. P x = P z"}
   |> kill_trivial_quantifiers
   |> pretty_term @{context} 
@@ -330,9 +330,9 @@
 text \<open>
   This function generates for example:
 
-  @{ML_matchresult_fake [display,gray] 
+  @{ML_response [display,gray] 
   \<open>pwriteln (pretty_term @{context} (term_tree 2))\<close> 
-  \<open>(1 + 2) + (3 + 4)\<close>} 
+  \<open>1 + 2 + (3 + 4)\<close>} 
 
   The next function constructs a goal of the form \<open>P \<dots>\<close> with a term 
   produced by @{ML term_tree} filled in.