--- a/ProgTutorial/Recipes/Sat.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/Sat.thy	Tue May 14 11:10:53 2019 +0200
@@ -71,7 +71,9 @@
   @{ML_response_fake [display,gray]
   "SAT_Solver.invoke_solver \"minisat\" pform"
   "SAT_Solver.SATISFIABLE assg"}
+*}
 
+text {*
   determines that the formula @{ML pform} is satisfiable. If we inspect
   the returned function @{text assg}
 
@@ -81,7 +83,7 @@
 in 
   (assg 1, assg 2, assg 3)
 end"
-  "(SOME true, SOME true, NONE)"}
+  "(NONE, SOME true, NONE)"}
 
   we obtain a possible assignment for the variables @{text "A"} an @{text "B"}
   that makes the formula satisfiable.