--- a/ProgTutorial/Recipes/Sat.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Tue May 21 14:37:39 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_matchresult_fake [display,gray]
+  @{ML_response [display,gray]
   \<open>Termtab.dest table\<close>
   \<open>[(Free ("A", "bool"), 1), (Free ("B", "bool"), 2)]\<close>}
 
@@ -58,9 +58,9 @@
   returns @{ML \<open>BoolVar 1\<close> in Prop_Logic} for  @{ML pform'} and the table 
   @{ML table'} is:
 
-  @{ML_matchresult_fake [display,gray]
-  \<open>map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')\<close>
-  \<open>(\<forall>x. P x, 1)\<close>}
+  @{ML_response [display,gray]
+  \<open>map (apfst (YXML.content_of o Syntax.string_of_term @{context})) (Termtab.dest table')\<close>
+  \<open>("\<forall>x. P x", 1)\<close>}
   
   In the print out of the tabel, we used some pretty printing scaffolding 
   to see better which assignment the table contains.