--- a/ProgTutorial/Solutions.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Solutions.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -2,19 +2,11 @@
 imports First_Steps "Recipes/Timing"
 begin
 
-(*<*)
-setup{*
-open_file_with_prelude 
-  "Solutions_Code.thy"
-  ["theory Solutions", "imports First_Steps", "begin"]
-*}
-(*>*)
-
 chapter {* Solutions to Most Exercises\label{ch:solutions} *}
 
 text {* \solution{fun:revsum} *}
 
-ML{*fun rev_sum 
+ML %grayML{*fun rev_sum 
   ((p as Const (@{const_name plus}, _)) $ t $ u) = p $ u $ rev_sum t
   | rev_sum t = t *}
 
@@ -22,7 +14,7 @@
   An alternative solution using the function @{ML_ind mk_binop in HOLogic} is:
  *}
 
-ML{*fun rev_sum t =
+ML %grayML{*fun rev_sum t =
 let
   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
     | dest_sum u = [u]
@@ -32,7 +24,7 @@
 
 text {* \solution{fun:makesum} *}
 
-ML{*fun make_sum t1 t2 =
+ML %grayML{*fun make_sum t1 t2 =
   HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
 text {* \solution{fun:killqnt} *}
@@ -75,7 +67,7 @@
 
 text {* \solution{fun:makelist} *}
 
-ML{*fun mk_rev_upto i = 
+ML %grayML{*fun mk_rev_upto i = 
   1 upto i
   |> map (HOLogic.mk_number @{typ int})
   |> HOLogic.mk_list @{typ int}
@@ -83,7 +75,7 @@
 
 text {* \solution{ex:debruijn} *}
 
-ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
+ML %grayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
 
 fun rhs 1 = P 1
   | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
@@ -97,7 +89,7 @@
 
 text {* \solution{ex:scancmts} *}
 
-ML{*val any = Scan.one (Symbol.not_eof)
+ML %grayML{*val any = Scan.one (Symbol.not_eof)
 
 val scan_cmt =
 let
@@ -130,7 +122,7 @@
 
 text {* \solution{ex:contextfree} *}
 
-ML{*datatype expr = 
+ML %grayML{*datatype expr = 
    Number of int
  | Mult of expr * expr 
  | Add of expr * expr
@@ -217,7 +209,7 @@
   de Bruijn formulae from Exercise \ref{ex:debruijn}.
 *}
 
-ML{*fun de_bruijn_prove ctxt n =
+ML %grayML{*fun de_bruijn_prove ctxt n =
 let 
   val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
 in
@@ -229,11 +221,11 @@
   You can use this function to prove de Bruijn formulae.
 *}
 
-ML{*de_bruijn_prove @{context} 3 *}
+ML %grayML{*de_bruijn_prove @{context} 3 *}
 
 text {* \solution{ex:addsimproc} *}
 
-ML{*fun dest_sum term =
+ML %grayML{*fun dest_sum term =
   case term of 
     (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
         (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
@@ -279,7 +271,7 @@
   exercise.
 *}
 
-ML{*fun add_simple_conv ctxt ctrm =
+ML %grayML{*fun add_simple_conv ctxt ctrm =
 let
   val trm = Thm.term_of ctrm
 in
@@ -323,7 +315,7 @@
   additions.
 *}
 
-ML{*fun term_tree n =
+ML %grayML{*fun term_tree n =
 let
   val count = Unsynchronized.ref 0; 
 
@@ -347,7 +339,7 @@
   produced by @{ML term_tree} filled in.
 *}
 
-ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}
+ML %grayML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}
 
 text {*
   Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
@@ -356,7 +348,7 @@
   then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
 *}
 
-ML{*local
+ML %grayML{*local
   fun mk_tac tac = 
         timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])
 in
@@ -369,7 +361,7 @@
   This is all we need to let the conversion run against the simproc:
 *}
 
-ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
+ML %grayML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
 val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}
 
 text {*