--- a/ProgTutorial/Essential.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Essential.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -2,15 +2,6 @@
 imports Base First_Steps
 begin
 
-(*<*)
-setup{*
-open_file_with_prelude 
-  "Essential_Code.thy"
-  ["theory Essential", "imports Base First_Steps", "begin"]
-*}
-(*>*)
-
-
 chapter {* Isabelle Essentials *}
 
 text {*
@@ -229,7 +220,7 @@
   detail in Section~\ref{sec:pretty}).
 *}
 
-ML{*local
+ML %grayML{*local
   fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
   fun pp_list xs = Pretty.list "[" "]" xs
   fun pp_str s   = Pretty.str s
@@ -251,7 +242,7 @@
   @{ML_ind addPrettyPrinter in PolyML} as follows.
 *}
 
-ML{*PolyML.addPrettyPrinter 
+ML %grayML{*PolyML.addPrettyPrinter 
   (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*}
 
 text {*
@@ -281,7 +272,7 @@
   with the code
 *}
 
-ML{*PolyML.addPrettyPrinter 
+ML %grayML{*PolyML.addPrettyPrinter 
   (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*}
 
 text {*
@@ -312,7 +303,7 @@
 
 *}
 
-ML{*fun make_imp P Q =
+ML %grayML{*fun make_imp P Q =
 let
   val x = Free ("x", @{typ nat})
 in 
@@ -325,7 +316,7 @@
   the following does \emph{not} work.
 *}
 
-ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
+ML %grayML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
 
 text {*
   To see this, apply @{text "@{term S}"} and @{text "@{term T}"} 
@@ -427,7 +418,7 @@
   function that strips off the outermost forall quantifiers in a term.
 *}
 
-ML{*fun strip_alls t =
+ML %grayML{*fun strip_alls t =
 let 
   fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))
 in
@@ -450,7 +441,7 @@
   builds the quantification from a body and a list of (free) variables.
 *}
   
-ML{*fun build_alls ([], t) = t
+ML %grayML{*fun build_alls ([], t) = t
   | build_alls (Free (x, T) :: vs, t) = 
       Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool}) 
         $ Abs (x, T, build_alls (vs, t))*}
@@ -549,7 +540,7 @@
   @{text is_true} as follows
 *}
 
-ML{*fun is_true @{term True} = true
+ML %grayML{*fun is_true @{term True} = true
   | is_true _ = false*}
 
 text {*
@@ -557,7 +548,7 @@
   the function 
 *}
 
-ML{*fun is_all (@{term All} $ _) = true
+ML %grayML{*fun is_all (@{term All} $ _) = true
   | is_all _ = false*}
 
 text {* 
@@ -571,7 +562,7 @@
   for this function is
 *}
 
-ML{*fun is_all (Const ("HOL.All", _) $ _) = true
+ML %grayML{*fun is_all (Const ("HOL.All", _) $ _) = true
   | is_all _ = false*}
 
 text {* 
@@ -586,7 +577,7 @@
   attempts to pick out @{text "Nil"}-terms:
 *}
 
-ML{*fun is_nil (Const ("Nil", _)) = true
+ML %grayML{*fun is_nil (Const ("Nil", _)) = true
   | is_nil _ = false *}
 
 text {* 
@@ -622,7 +613,7 @@
   be written as follows.
 *}
 
-ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
+ML %grayML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
   | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
   | is_nil_or_all _ = false *}
 
@@ -640,18 +631,18 @@
 
 *} 
 
-ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
+ML %grayML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
 
 text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *}
 
-ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
+ML %grayML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
 
 text {*
   If you want to construct a function type with more than one argument
   type, then you can use @{ML_ind "--->" in Term}.
 *}
 
-ML{*fun make_fun_types tys ty = tys ---> ty *}
+ML %grayML{*fun make_fun_types tys ty = tys ---> ty *}
 
 text {*
   A handy function for manipulating terms is @{ML_ind map_types in Term}: it takes a 
@@ -659,7 +650,7 @@
   change every @{typ nat} in a term into an @{typ int} using the function:
 *}
 
-ML{*fun nat_to_int ty =
+ML %grayML{*fun nat_to_int ty =
   (case ty of
      @{typ nat} => @{typ int}
    | Type (s, tys) => Type (s, map nat_to_int tys)
@@ -802,7 +793,7 @@
   \begin{figure}[t]
   \begin{minipage}{\textwidth}
   \begin{isabelle}*}
-ML{*fun pretty_helper aux env =
+ML %grayML{*fun pretty_helper aux env =
   env |> Vartab.dest  
       |> map aux
       |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2]) 
@@ -864,7 +855,7 @@
 class s1
 class s2 
 
-ML{*val (tyenv, index) = let
+ML %grayML{*val (tyenv, index) = let
   val ty1 = @{typ_pat "?'a::s1"}
   val ty2 = @{typ_pat "?'b::s2"}
 in
@@ -916,7 +907,7 @@
   of failure. For example
 *}
 
-ML{*val tyenv_match = let
+ML %grayML{*val tyenv_match = let
   val pat = @{typ_pat "?'a * ?'b"}
   and ty  = @{typ_pat "bool list * nat"}
 in
@@ -944,7 +935,7 @@
   following matcher:
 *}
 
-ML{*val tyenv_match' = let
+ML %grayML{*val tyenv_match' = let
   val pat = @{typ_pat "?'a * ?'b"}
   and ty  = @{typ_pat "?'b list * nat"}
 in
@@ -989,7 +980,7 @@
   the function @{text "pretty_env"}:
 *}
 
-ML{*fun pretty_env ctxt env =
+ML %grayML{*fun pretty_env ctxt env =
 let
   fun get_trms (v, (T, t)) = (Var (v, T), t) 
   val print = pairself (pretty_term ctxt)
@@ -1004,7 +995,7 @@
   @{text "?X ?Y"}.
 *}
 
-ML{*val (_, fo_env) = let
+ML %grayML{*val (_, fo_env) = let
   val fo_pat = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
   val trm_a = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"} 
   val trm_b = @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}
@@ -1123,7 +1114,7 @@
   list of potentially infinite unifiers.  An example is as follows
 *}
 
-ML{*val uni_seq =
+ML %grayML{*val uni_seq =
 let 
   val trm1 = @{term_pat "?X ?Y"}
   val trm2 = @{term "f a"}
@@ -1138,7 +1129,7 @@
   unifiers @{text "un1\<dots>un3"}.
 *}
 
-ML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;
+ML %grayML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;
 val SOME ((un2, _), next2) = Seq.pull next1;
 val SOME ((un3, _), next3) = Seq.pull next2;
 val NONE = Seq.pull next3 *}
@@ -1226,14 +1217,14 @@
   @{ML_type ctyp}-pairs with the function
 *}
 
-ML{*fun prep_trm thy (x, (T, t)) = 
+ML %grayML{*fun prep_trm thy (x, (T, t)) = 
   (cterm_of thy (Var (x, T)), cterm_of thy t)*} 
 
 text {*
   and into proper @{ML_type cterm}-pairs with
 *}
 
-ML{*fun prep_ty thy (x, (S, ty)) = 
+ML %grayML{*fun prep_ty thy (x, (S, ty)) = 
   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*}
 
 text {*
@@ -1628,7 +1619,7 @@
   To see how it works let us assume we defined our own theorem list @{text MyThmList}.
 *}
 
-ML{*structure MyThmList = Generic_Data
+ML %grayML{*structure MyThmList = Generic_Data
   (type T = thm list
    val empty = []
    val extend = I
@@ -1809,7 +1800,7 @@
   following function for atomizing a theorem.
 *}
 
-ML{*fun atomize_thm thm =
+ML %grayML{*fun atomize_thm thm =
 let
   val thm' = forall_intr_vars thm
   val thm'' = Object_Logic.atomize (cprop_of thm')
@@ -1850,7 +1841,7 @@
   following three helper functions.
 *}
 
-ML{*fun rep_goals i = replicate i @{prop "f x = f x"}
+ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"}
 fun rep_tacs i = replicate i (rtac @{thm refl})
 
 fun multi_test ctxt i =
@@ -1871,7 +1862,7 @@
   using @{ML map} and @{ML prove in Goal}.
 *}
   
-ML{*let 
+ML %grayML{*let 
   fun test_prove ctxt thm =
     Goal.prove ctxt ["P", "x"] [] thm (K (rtac @{thm refl} 1))
 in
@@ -2040,7 +2031,7 @@
   and uses them as name in the outermost abstractions.
 *}
 
-ML{*fun rename_allq [] t = t
+ML %grayML{*fun rename_allq [] t = t
   | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = 
       Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)
   | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =
@@ -2117,7 +2108,7 @@
   this attribute is
 *}
 
-ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
+ML %grayML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
 
 text {* 
   where the function @{ML_ind  rule_attribute in Thm} expects a function taking a 
@@ -2164,7 +2155,7 @@
   attribute as follows:
 *}
 
-ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
+ML %grayML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
   "applying the sym rule" *}
 
 text {*
@@ -2178,7 +2169,7 @@
   after another). The code for this attribute is
 *}
 
-ML{*fun MY_THEN thms = 
+ML %grayML{*fun MY_THEN thms = 
 let
   fun RS_rev thm1 thm2 = thm2 RS thm1
 in
@@ -2237,7 +2228,7 @@
   let us introduce a theorem list.
 *}
 
-ML{*structure MyThms = Named_Thms
+ML %grayML{*structure MyThms = Named_Thms
   (val name = @{binding "attr_thms"} 
    val description = "Theorems for an Attribute") *}
 
@@ -2248,7 +2239,7 @@
   with the code
 *}
 
-ML{*val my_add = Thm.declaration_attribute MyThms.add_thm
+ML %grayML{*val my_add = Thm.declaration_attribute MyThms.add_thm
 val my_del = Thm.declaration_attribute MyThms.del_thm *}
 
 text {* 
@@ -2342,7 +2333,7 @@
   type:
 *}
 
-ML{*fun pprint prt = tracing (Pretty.string_of prt)*}
+ML %grayML{*fun pprint prt = tracing (Pretty.string_of prt)*}
 
 text {*
   The point of the pretty-printing infrastructure is to give hints about how to
@@ -2351,13 +2342,13 @@
   following function that replicates a string n times:
 *}
 
-ML{*fun rep n str = implode (replicate n str) *}
+ML %grayML{*fun rep n str = implode (replicate n str) *}
 
 text {*
   and suppose we want to print out the string:
 *}
 
-ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
+ML %grayML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
 
 text {*
   We deliberately chose a large string so that it spans over more than one line.