diff -r 6103b0eadbf2 -r f7c97e64cc2a ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Solutions.thy	Thu May 16 19:56:12 2019 +0200
@@ -55,7 +55,7 @@
   \<open>-1\<close> to account for the deleted quantifier. An example is 
   as follows:
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "@{prop \"\<forall>x y z. P x = P z\"}
   |> kill_trivial_quantifiers
   |> pretty_term @{context} 
@@ -110,7 +110,7 @@
   @{ML scan_all} retruns a string, instead of the pair a parser would
   normally return. For example:
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
 "let
   val input1 = (Symbol.explode \"foo bar\")
   val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\")
@@ -330,7 +330,7 @@
 text \<open>
   This function generates for example:
 
-  @{ML_response_fake [display,gray] 
+  @{ML_matchresult_fake [display,gray] 
   "pwriteln (pretty_term @{context} (term_tree 2))" 
   "(1 + 2) + (3 + 4)"}