--- a/ProgTutorial/Recipes/Sat.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Recipes/Sat.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -27,7 +27,7 @@
   The function will return a propositional formula and a table. Suppose 
 *}
 
-ML{*val (pform, table) = 
+ML %grayML{*val (pform, table) = 
        Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty*}
 
 text {*
@@ -51,7 +51,7 @@
   Attempting to translate @{term "\<forall>x::nat. P x"}
 *}
 
-ML{*val (pform', table') = 
+ML %grayML{*val (pform', table') = 
        Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty*}
 
 text {*
@@ -121,4 +121,4 @@
 *}
 
 
-end
\ No newline at end of file
+end