--- a/ProgTutorial/First_Steps.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/First_Steps.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -2,13 +2,6 @@
 imports Base
 begin
 
-(*<*)
-setup{*
-open_file_with_prelude 
-  "First_Steps_Code.thy"
-  ["theory First_Steps", "imports Main", "begin"]
-*}
-(*>*)
 
 chapter {* First Steps\label{chp:firststeps} *}
 
@@ -161,7 +154,7 @@
   @{ML_struct Syntax}. For more convenience, we bind them to the toplevel.
 *}
 
-ML{*val pretty_term = Syntax.pretty_term
+ML %grayML{*val pretty_term = Syntax.pretty_term
 val pwriteln = Pretty.writeln*}
 
 text {*
@@ -176,7 +169,7 @@
   to separate them.
 *} 
 
-ML{*fun pretty_terms ctxt trms =  
+ML %grayML{*fun pretty_terms ctxt trms =  
   Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
 
 text {*
@@ -185,7 +178,7 @@
   @{ML_ind show_types in Syntax} to @{ML true}.
 *}
 
-ML{*val show_types_ctxt = Config.put show_types true @{context}*}
+ML %grayML{*val show_types_ctxt = Config.put show_types true @{context}*}
 
 text {*
   Now by using this context @{ML pretty_term} prints out
@@ -222,7 +215,7 @@
   A @{ML_type cterm} can be printed with the following function.
 *}
 
-ML{*fun pretty_cterm ctxt ctrm =  
+ML %grayML %grayML{*fun pretty_cterm ctxt ctrm =  
   pretty_term ctxt (term_of ctrm)*}
 
 text {*
@@ -231,7 +224,7 @@
   printed again with @{ML commas in Pretty}.
 *} 
 
-ML{*fun pretty_cterms ctxt ctrms =  
+ML %grayML{*fun pretty_cterms ctxt ctrms =  
   Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))*}
 
 text {*
@@ -239,7 +232,7 @@
   into a @{ML_type term} using the function @{ML_ind prop_of in Thm}. 
 *}
 
-ML{*fun pretty_thm ctxt thm =
+ML %grayML{*fun pretty_thm ctxt thm =
   pretty_term ctxt (prop_of thm)*}
 
 text {*
@@ -257,7 +250,7 @@
   can switch off the question marks as follows:
 *}
 
-ML{*fun pretty_thm_no_vars ctxt thm =
+ML %grayML{*fun pretty_thm_no_vars ctxt thm =
 let
   val ctxt' = Config.put show_question_marks false ctxt
 in
@@ -275,7 +268,7 @@
   with printing more than one theorem. 
 *}
 
-ML{*fun pretty_thms ctxt thms =  
+ML %grayML{*fun pretty_thms ctxt thms =  
   Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))
 
 fun pretty_thms_no_vars ctxt thms =  
@@ -285,7 +278,7 @@
   Printing functions for @{ML_type typ} are
 *}
 
-ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
+ML %grayML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
 fun pretty_typs ctxt tys = 
   Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*}
 
@@ -293,7 +286,7 @@
   respectively @{ML_type ctyp}
 *}
 
-ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
+ML %grayML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
 fun pretty_ctyps ctxt ctys = 
   Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*}
 
@@ -355,13 +348,13 @@
   identity function defined as
 *}
 
-ML{*fun I x = x*}
+ML %grayML{*fun I x = x*}
 
 text {* 
   Another simple combinator is @{ML_ind K in Library}, defined as 
 *}
 
-ML{*fun K x = fn _ => x*}
+ML %grayML{*fun K x = fn _ => x*}
 
 text {*
   @{ML K} ``wraps'' a function around @{text "x"} that ignores its argument. As a 
@@ -370,7 +363,7 @@
   The next combinator is reverse application, @{ML_ind  "|>" in Basics}, defined as: 
 *}
 
-ML{*fun x |> f = f x*}
+ML %grayML{*fun x |> f = f x*}
 
 text {* While just syntactic sugar for the usual function application,
   the purpose of this combinator is to implement functions in a  
@@ -394,16 +387,16 @@
   the reverse application is much clearer than writing
 *}
 
-ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
+ML %grayML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
 
 text {* or *}
 
-ML{*fun inc_by_five x = 
+ML %grayML{*fun inc_by_five x = 
   ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
 
 text {* and typographically more economical than *}
 
-ML{*fun inc_by_five x =
+ML %grayML{*fun inc_by_five x =
 let val y1 = x + 1
     val y2 = (y1, y1)
     val y3 = fst y2
@@ -477,7 +470,7 @@
   It can be used to define the following function
 *}
 
-ML{*val inc_by_six = 
+ML %grayML{*val inc_by_six = 
   (fn x => x + 1) #> 
   (fn x => x + 2) #> 
   (fn x => x + 3)*}
@@ -535,13 +528,13 @@
   value (as a pair). It is defined as
 *}
 
-ML{*fun `f = fn x => (f x, x)*}
+ML %grayML{*fun `f = fn x => (f x, x)*}
 
 text {*
   An example for this combinator is the function
 *}
 
-ML{*fun inc_as_pair x =
+ML %grayML{*fun inc_as_pair x =
      x |> `(fn x => x + 1)
        |> (fn (x, y) => (x, y + 1))*}
 
@@ -556,13 +549,13 @@
   the first component of the pair, defined as
 *}
 
-ML{*fun (x, y) |>> f = (f x, y)*}
+ML %grayML{*fun (x, y) |>> f = (f x, y)*}
 
 text {*
   and the second combinator to the second component, defined as
 *}
 
-ML{*fun (x, y) ||> f = (x, f y)*}
+ML %grayML{*fun (x, y) ||> f = (x, f y)*}
 
 text {*
   These two functions can, for example, be used to avoid explicit @{text "lets"} for
@@ -573,7 +566,7 @@
   implemented as
 *}
 
-ML{*fun separate i [] = ([], [])
+ML %grayML{*fun separate i [] = ([], [])
   | separate i (x::xs) =
       let 
         val (los, grs) = separate i xs
@@ -587,7 +580,7 @@
   can be implemented more concisely as
 *}
 
-ML{*fun separate i [] = ([], [])
+ML %grayML{*fun separate i [] = ([], [])
   | separate i (x::xs) =
       if i <= x 
       then separate i xs ||> cons x
@@ -602,14 +595,14 @@
   elements from a pair. This combinator is defined as
 *}
 
-ML{*fun (x, y) |-> f = f x y*}
+ML %grayML{*fun (x, y) |-> f = f x y*}
 
 text {* 
   and can be used to write the following roundabout version 
   of the @{text double} function: 
 *}
 
-ML{*fun double x =
+ML %grayML{*fun double x =
       x |>  (fn x => (x, x))
         |-> (fn x => fn y => x + y)*}
 
@@ -670,7 +663,7 @@
   A more realistic example for this combinator is the following code
 *}
 
-ML{*val (((one_def, two_def), three_def), ctxt') = 
+ML %grayML{*val (((one_def, two_def), three_def), ctxt') = 
   @{context}
   |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) 
   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
@@ -703,7 +696,7 @@
   function @{text double} can also be written as:
 *}
 
-ML{*val double =
+ML %grayML{*val double =
    (fn x => (x, x)) #-> 
    (fn x => fn y => x + y)*}
 
@@ -801,7 +794,7 @@
   determined at ``compile-time'', not at ``run-time''. For example the function
 *}
 
-ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
+ML %grayML{*fun not_current_thyname () = Context.theory_name @{theory} *}
 
 text {*
   does \emph{not} return the name of the current theory, if it is run in a 
@@ -856,7 +849,7 @@
   and the second is a proof. For example
 *}
 
-ML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
+ML %grayML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
 
 text {*
   The result can be printed out as follows.
@@ -871,7 +864,7 @@
   simpset.
 *}
 
-ML{*fun get_thm_names_from_ss simpset =
+ML %grayML{*fun get_thm_names_from_ss simpset =
 let
   val {simps,...} = Raw_Simplifier.dest_ss simpset
 in
@@ -936,7 +929,7 @@
   we can write an antiquotation for type patterns. Its code is
 *}
 
-ML{*val type_pat_setup = 
+ML %grayML{*val type_pat_setup = 
 let
   val parser = Args.context -- Scan.lift Args.name_source
 
@@ -999,7 +992,7 @@
   functions for booleans and integers into and from the type @{ML_type Universal.universal}.
 *}
 
-ML{*local
+ML %grayML{*local
   val fn_int  = Universal.tag () : int  Universal.tag
   val fn_bool = Universal.tag () : bool Universal.tag
 in
@@ -1015,7 +1008,7 @@
   then store them in a @{ML_type "Universal.universal list"} as follows:
 *}
 
-ML{*val foo_list = 
+ML %grayML{*val foo_list = 
 let
   val thirteen = inject_int 13
   val truth_val = inject_bool true
@@ -1089,7 +1082,7 @@
   auxiliary functions, which help us with accessing the table.
 *}
 
-ML{*val lookup = Symtab.lookup o Data.get
+ML %grayML{*val lookup = Symtab.lookup o Data.get
 fun update k v = Data.map (Symtab.update (k, v))*}
 
 text {*
@@ -1134,7 +1127,7 @@
   integers.
 *}
 
-ML{*structure WrongRefData = Theory_Data
+ML %grayML{*structure WrongRefData = Theory_Data
   (type T = (int list) Unsynchronized.ref
    val empty = Unsynchronized.ref []
    val extend = I
@@ -1151,7 +1144,7 @@
   For updating the reference we use the following function
 *}
 
-ML{*fun ref_update n = WrongRefData.map 
+ML %grayML{*fun ref_update n = WrongRefData.map 
       (fn r => let val _ = r := n::(!r) in r end)*}
 
 text {*
@@ -1202,7 +1195,7 @@
   following code we can store a list of terms in a proof context.
 *}
 
-ML{*structure Data = Proof_Data
+ML %grayML{*structure Data = Proof_Data
   (type T = term list
    fun init _ = [])*}
 
@@ -1214,7 +1207,7 @@
   term and printing the list. 
 *}
 
-ML{*fun update trm = Data.map (fn trms => trm::trms)
+ML %grayML{*fun update trm = Data.map (fn trms => trm::trms)
 
 fun print ctxt =
   case (Data.get ctxt) of
@@ -1272,7 +1265,7 @@
   is such a common task.  To obtain a named theorem list, you just declare
 *}
 
-ML{*structure FooRules = Named_Thms
+ML %grayML{*structure FooRules = Named_Thms
   (val name = @{binding "foo"} 
    val description = "Theorems for foo") *}
 
@@ -1339,7 +1332,7 @@
   values can be declared by
 *}
 
-ML{*val bval = Attrib.setup_config_bool @{binding "bval"} (K false)
+ML %grayML{*val bval = Attrib.setup_config_bool @{binding "bval"} (K false)
 val ival = Attrib.setup_config_int @{binding "ival"} (K 0)
 val sval = Attrib.setup_config_string @{binding "sval"} (K "some string") *}