diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Recipes/Sat.thy
--- a/ProgTutorial/Recipes/Sat.thy	Tue May 21 16:22:30 2019 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Wed May 22 12:38:51 2019 +0200
@@ -52,14 +52,16 @@
 \<close>
 
 ML %grayML\<open>val (pform', table') = 
-       Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty\<close>
+  Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"}
+  Termtab.empty\<close>
 
 text \<open>
   returns @{ML \<open>BoolVar 1\<close> in Prop_Logic} for  @{ML pform'} and the table 
   @{ML table'} is:
 
   @{ML_response [display,gray]
-  \<open>map (apfst (YXML.content_of o Syntax.string_of_term @{context})) (Termtab.dest table')\<close>
+  \<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