--- a/ProgTutorial/Recipes/Sat.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Thu May 16 19:56:12 2019 +0200
@@ -42,7 +42,7 @@
   (appropriately updated) in the result. In the case above the
   input table is empty (i.e.~@{ML Termtab.empty}) and the output table is
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "Termtab.dest table"
   "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}
 
@@ -58,7 +58,7 @@
   returns @{ML "BoolVar 1" in Prop_Logic} for  @{ML pform'} and the table 
   @{ML table'} is:
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
   "(\<forall>x. P x, 1)"}
   
@@ -68,7 +68,7 @@
   Having produced a propositional formula, you can now call the SAT solvers 
   with the function @{ML "SAT_Solver.invoke_solver"}. For example
 
-  @{ML_response_fake [display,gray]
+  @{ML_matchresult_fake [display,gray]
   "SAT_Solver.invoke_solver \"minisat\" pform"
   "SAT_Solver.SATISFIABLE assg"}
 \<close>
@@ -77,7 +77,7 @@
   determines that the formula @{ML pform} is satisfiable. If we inspect
   the returned function \<open>assg\<close>
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
 "let
   val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform
 in