--- a/ProgTutorial/Advanced.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Advanced.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -2,14 +2,6 @@
 imports Base First_Steps
 begin
 
-(*<*)
-setup{*
-open_file_with_prelude 
-  "Advanced_Code.thy"
-  ["theory Advanced", "imports Base First_Steps", "begin"]
-*}
-(*>*)
-
 
 chapter {* Advanced Isabelle\label{chp:advanced} *}
 
@@ -82,7 +74,7 @@
 
 *}  
 
-ML{*let
+ML %grayML{*let
   val thy = @{theory}
   val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
 in 
@@ -256,7 +248,7 @@
   for a context. The above proof fragment corresponds roughly to the following ML-code
 *}
 
-ML{*val ctxt0 = @{context};
+ML %grayML{*val ctxt0 = @{context};
 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0;
 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*}
 
@@ -526,8 +518,8 @@
 
 
 (*
-ML{*Proof_Context.debug := true*}
-ML{*Proof_Context.verbose := true*}
+ML %grayML{*Proof_Context.debug := true*}
+ML %grayML{*Proof_Context.verbose := true*}
 *)
 
 (*
@@ -600,20 +592,20 @@
   The simplest morphism is the  @{ML_ind identity in Morphism}-morphism defined as
 *}
 
-ML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*}
+ML %grayML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*}
   
 text {*
   Morphisms can be composed with the function @{ML_ind "$>" in Morphism}
 *}
 
-ML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T) 
+ML %grayML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T) 
   | trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t)
   | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s)
   | trm_phi t = t*}
 
-ML{*val phi = Morphism.term_morphism trm_phi*}
+ML %grayML{*val phi = Morphism.term_morphism trm_phi*}
 
-ML{*Morphism.term phi @{term "P x y"}*}
+ML %grayML{*Morphism.term phi @{term "P x y"}*}
 
 text {*
   @{ML_ind term_morphism in Morphism}

--- a/ProgTutorial/Appendix.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Appendix.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -3,14 +3,6 @@
 imports Base
 begin
 
-(*<*)
-setup{*
-open_file_with_prelude 
-  "Recipes_Code.thy"
-  ["theory Recipes", "imports Main", "begin"]
-*}
-(*>*)
-
 text {* \appendix *}
 
 
@@ -31,4 +23,4 @@
   \end{itemize}
 *}
 
-end
\ No newline at end of file
+end

--- a/ProgTutorial/Base.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Base.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -12,117 +12,6 @@
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
-
-(* re-definition of various ML antiquotations     *)
-(* to have a special tag for text enclosed in ML; *)
-(* they also write the code into a separate file  *)
-
-ML {*
-val filename = Attrib.setup_config_string @{binding "filename"} (K "File_Code.ML")
-*}
-
-
-ML {*
-fun write_file txt thy =
-let 
-  val stream = Config.get_global thy filename
-               |> TextIO.openAppend 
-in
-  TextIO.output (stream, txt); 
-  TextIO.flushOut stream;       (* needed ?*)
-  TextIO.closeOut stream
-end
-*}
-
-ML {*
-fun write_file_ml_blk txt thy =
-let
-  val pre  = implode ["\n", "ML ", "{", "*", "\n"]
-  val post = implode ["\n", "*", "}", "\n"]
-  val _ = write_file (enclose pre post txt) thy
-in
-  thy
-end
-
-fun write_file_setup_blk txt thy =
-let
-  val pre  = implode ["\n", "setup ", "{", "*", "\n"]
-  val post = implode ["\n", "*", "}", "\n"]
-  val _ = write_file (enclose pre post txt) thy
-in
-  thy
-end
-
-fun write_file_lsetup_blk txt lthy =
-let
-  val pre  = implode ["\n", "local_setup ", "{", "*", "\n"]
-  val post = implode ["\n", "*", "}", "\n"]
-  val _ = write_file (enclose pre post txt) (Proof_Context.theory_of lthy)
-in
-  lthy
-end
-
-*}
-
-ML {*
-fun open_file name thy =
-let  
-  val _ = tracing ("Open File: " ^ name)
-  val _ = TextIO.openOut name
-in 
-  Config.put_global filename name thy
-end
-*}
-
-ML {*
-fun open_file_with_prelude name txts thy =
-let 
-  val thy' = open_file name thy 
-  val _ = write_file (cat_lines txts) thy'
-in
-  thy'
-end
-*}
-
-ML {*
-val _ =
-  Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl)
-    "ML text within theory or local theory"
-    (Parse.ML_source >> (fn (txt, pos) =>
-      Toplevel.generic_theory
-        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
-          Local_Theory.propagate_ml_env #> Context.map_theory (write_file_ml_blk txt))))
-*}
-
-ML {*
-val _ =
-  Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof"
-    (Parse.ML_source >> (fn (txt, pos) =>
-      Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
-*}
-
-
-ML {*
-val _ =
-  Outer_Syntax.command ("ML_val", Keyword.tag "TutorialML" Keyword.diag) "diagnostic ML text" 
-    (Parse.ML_source >> Isar_Cmd.ml_diag true)
-*}
-
-ML {*
-val _ =
-  Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup" 
-      (Parse.ML_source >> (fn (txt, pos) => 
-        (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
-*}
-
-ML {*
-val _ =
-  Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup" 
-      (Parse.ML_source >> (fn (txt, pos) => 
-         Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
-*}
-
 ML {*
 fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
 

--- 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. 

--- 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") *}
 

--- a/ProgTutorial/Intro.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Intro.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -2,14 +2,6 @@
 imports Base
 begin
 
-(*<*)
-setup{*
-open_file_with_prelude 
-  "Intro_Code.thy"
-  ["theory Intro", "imports Main", "begin"]
-*}
-(*>*)
-
 chapter {* Introduction *}
 
 text {*

--- a/ProgTutorial/Package/Ind_Code.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -213,7 +213,7 @@
   quantifiers. 
 *}
 
-ML{*fun inst_spec ctrm =
+ML %grayML{*fun inst_spec ctrm =
 let
   val cty = ctyp_of_term ctrm
 in 
@@ -227,7 +227,7 @@
   tactic.\label{fun:instspectac}.
 *}
 
-ML{*fun inst_spec_tac ctrms = 
+ML %grayML{*fun inst_spec_tac ctrms = 
   EVERY' (map (dtac o inst_spec) ctrms)*}
 
 text {*
@@ -478,7 +478,7 @@
   our work here, we use the following two helper functions.
 *}
 
-ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
+ML %grayML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}
 
 text {* 
@@ -588,7 +588,7 @@
 \begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
-ML{*fun chop_print params1 params2 prems1 prems2 ctxt =
+ML %grayML{*fun chop_print params1 params2 prems1 prems2 ctxt =
 let 
  val pps = [Pretty.big_list "Params1 from the rule:" (map (pretty_cterm ctxt) params1), 
             Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), 
@@ -744,7 +744,7 @@
   we can implement the following function
 *}
 
-ML{*fun prepare_prem params2 prems2 prem =  
+ML %grayML{*fun prepare_prem params2 prems2 prem =  
   rtac (case prop_of prem of
            _ $ (Const (@{const_name All}, _) $ _) =>
                  prem |> all_elims params2 
@@ -758,7 +758,7 @@
   tactic will therefore prove the lemma completely.
 *}
 
-ML{*fun prove_intro_tac i preds rules =
+ML %grayML{*fun prove_intro_tac i preds rules =
   SUBPROOF (fn {params, prems, ...} =>
   let
     val cparams = map snd params
@@ -945,7 +945,7 @@
   three wrappers this function:
 *}
 
-ML{*fun note_many qname ((name, attrs), thms) = 
+ML %grayML{*fun note_many qname ((name, attrs), thms) = 
   Local_Theory.note ((Binding.qualify false qname name, attrs), thms) 
 
 fun note_single1 qname ((name, attrs), thm) = 
@@ -1030,4 +1030,4 @@
   Why the mut-name? 
   What does @{ML Binding.qualify} do?}
 *}
-(*<*)end(*>*)
\ No newline at end of file
+(*<*)end(*>*)

--- a/ProgTutorial/Package/Ind_Extensions.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -192,10 +192,10 @@
 
 text {* Type declarations *}
 
-ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
+ML %grayML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
 
-ML{*fun pat_completeness_auto ctxt =
+ML %grayML{*fun pat_completeness_auto ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1
     THEN auto_tac ctxt*}
 
@@ -213,4 +213,4 @@
     [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})]
       conf pat_completeness_auto #> snd*}
 
-(*<*)end(*>*)
\ No newline at end of file
+(*<*)end(*>*)

--- a/ProgTutorial/Package/Ind_General_Scheme.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -197,7 +197,7 @@
 \begin{figure}[p]
 \begin{minipage}{\textwidth}
 \begin{isabelle}*}  
-ML{*(* even-odd example *)
+ML %grayML{*(* even-odd example *)
 val eo_defs = [@{thm even_def}, @{thm odd_def}]
 
 val eo_rules =  

--- a/ProgTutorial/Package/Ind_Interface.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -61,7 +61,7 @@
 
 *}
 
-ML{*val spec_parser = 
+ML %grayML{*val spec_parser = 
    Parse.fixes -- 
    Scan.optional 
      (Parse.$$$ "where" |--
@@ -177,4 +177,4 @@
   introduction rules. The description of this function will span over
   the next two sections.
 *}
-(*<*)end(*>*)
\ No newline at end of file
+(*<*)end(*>*)

--- a/ProgTutorial/Package/Ind_Intro.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Package/Ind_Intro.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -2,13 +2,6 @@
 imports "../Base"
 begin
 
-(*<*)
-setup{*
-open_file_with_prelude 
-  "Ind_Package_Code.thy"
-  ["theory Ind_Package", "imports Main", "begin"]
-*}
-(*>*)
 
 chapter {* How to Write a Definitional Package\label{chp:package} *}
 

--- a/ProgTutorial/Parsing.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -2,16 +2,6 @@
 imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"
 begin
 
-(*<*)
-setup {*
-open_file_with_prelude 
-"Parsing_Code.thy"
-["theory Parsing", 
- "imports Base \"Package/Simple_Inductive_Package\"", 
- "begin"]
-*}
-(*>*)
-
 chapter {* Parsing\label{chp:parsing} *}
 
 text {*
@@ -253,7 +243,7 @@
   of parsing @{text "p"}-followed-by-@{text "q"}, then you have to write:
 *}
 
-ML{*fun p_followed_by_q p q r =
+ML %grayML{*fun p_followed_by_q p q r =
 let 
   val err_msg = fn _ => p ^ " is not followed by " ^ q
 in
@@ -389,7 +379,7 @@
   datatype:
 *}
 
-ML{*datatype tree = 
+ML %grayML{*datatype tree = 
     Lf of string 
   | Br of tree * tree*}
 
@@ -399,7 +389,7 @@
   leaf---you might implement the following parser.
 *}
 
-ML{*fun parse_basic s = 
+ML %grayML{*fun parse_basic s = 
   $$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")"  
 
 and parse_tree s = 
@@ -434,7 +424,7 @@
   as follows.
 *}
 
-ML{*fun parse_basic s xs = 
+ML %grayML{*fun parse_basic s xs = 
   ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs 
 
 and parse_tree s xs = 
@@ -472,7 +462,7 @@
   tokens, not strings.  These token parsers have the type:
 *}
   
-ML{*type 'a parser = Token.T list -> 'a * Token.T list*}
+ML %grayML{*type 'a parser = Token.T list -> 'a * Token.T list*}
 
 text {*
   {\bf REDO!!}
@@ -512,7 +502,7 @@
   @{ML_ind define in Keyword}. For example calling it with 
 *}
 
-ML{*val _ = Keyword.define ("hello", NONE) *}
+ML %grayML{*val _ = Keyword.define ("hello", NONE) *}
 
 text {*
   then lexing @{text [quotes] "hello world"} will produce
@@ -538,7 +528,7 @@
   For convenience we define the function:
 *}
 
-ML{*fun filtered_input str = 
+ML %grayML{*fun filtered_input str = 
   filter Token.is_proper (Outer_Syntax.scan Position.none str) *}
 
 text {* 
@@ -630,7 +620,7 @@
   The following function will help to run examples.
 *}
 
-ML{*fun parse p input = Scan.finite Token.stopper (Scan.error p) input *}
+ML %grayML{*fun parse p input = Scan.finite Token.stopper (Scan.error p) input *}
 
 text {*
   The function @{ML_ind "!!!" in Parse} can be used to force termination
@@ -665,7 +655,7 @@
   modify the function @{ML filtered_input}, described earlier, as follows 
 *}
 
-ML{*fun filtered_input' str = 
+ML %grayML{*fun filtered_input' str = 
        filter Token.is_proper (Outer_Syntax.scan (Position.line 7) str) *}
 
 text {*
@@ -959,7 +949,7 @@
   defined as:
 *}
 
-ML{*let
+ML %grayML{*let
   val do_nothing = Scan.succeed (Local_Theory.background_theory I)
   val kind = Keyword.thy_decl
 in
@@ -1104,7 +1094,7 @@
   the function @{ML_ind define in Keyword}. For example:
 *}
 
-ML{*val _ = Keyword.define ("blink", NONE) *}
+ML %grayML{*val _ = Keyword.define ("blink", NONE) *}
 
 text {*
   At the moment the command \isacommand{foobar} is not very useful. Let us
@@ -1121,7 +1111,7 @@
   finally does nothing. For this you can write:
 *}
 
-ML{*let
+ML %grayML{*let
   fun trace_prop str = 
      Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
 
@@ -1214,7 +1204,7 @@
 val result_cookie = (Result.get, Result.put, "Result.put")
 *}
 
-ML{*let
+ML %grayML{*let
    fun after_qed thm_name thms lthy =
         Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 

--- a/ProgTutorial/Recipes/Antiquotes.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -113,7 +113,7 @@
   function will do this:
 *}
 
-ML{*fun ml_pat (code_txt, pat) =
+ML %grayML{*fun ml_pat (code_txt, pat) =
 let val pat' = 
          implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
 in 
@@ -125,7 +125,7 @@
 *}
 
 
-ML{*fun add_resp pat = map (fn s => "> " ^ s) pat*}
+ML %grayML{*fun add_resp pat = map (fn s => "> " ^ s) pat*}
 
 text {* 
   The rest of the code of @{text "ML_resp"} is: 
@@ -172,4 +172,4 @@
   values that are abstract datatypes, like @{ML_type thm}s and @{ML_type cterm}s.
 
 *}
-end
\ No newline at end of file
+end

--- a/ProgTutorial/Recipes/CallML.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Recipes/CallML.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -43,7 +43,7 @@
   @{const factor}. Here is a trivial definition in ML: 
 *}
 
-ML{*fun factor n = if n = 4 then 2 else 1*}
+ML %grayML{*fun factor n = if n = 4 then 2 else 1*}
 
 text{* 
   Of course this trivial definition of @{const factor} could have been given
@@ -98,7 +98,7 @@
 *}
 
 consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*)
-ML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*)
+ML %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*)
 code_const factor2 (SML "factor2")
 
 value "factor2 4"
@@ -136,7 +136,7 @@
   write ML-code that uses this datatype: 
 *}
 
-ML{*fun factor' n = if n = 4 then Result.Factor 2 else Result.Prime*}
+ML %grayML{*fun factor' n = if n = 4 then Result.Factor 2 else Result.Prime*}
 
 text{* 
   Finally we can link the HOL and ML version of @{const factor'} as
@@ -158,4 +158,4 @@
 value "factor' 4"
 
 end
-(*>*)
\ No newline at end of file
+(*>*)

--- a/ProgTutorial/Recipes/ExternalSolver.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -50,4 +50,4 @@
 *}
 
 
-end
\ No newline at end of file
+end

--- a/ProgTutorial/Recipes/Oracle.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Recipes/Oracle.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -122,7 +122,7 @@
   To be able to use our oracle for Isar proofs, we wrap it into a tactic:
 *}
 
-ML{*val iff_oracle_tac =
+ML %grayML{*val iff_oracle_tac =
   CSUBGOAL (fn (goal, i) => 
     (case try iff_oracle goal of
       NONE => no_tac

--- 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

--- a/ProgTutorial/Recipes/TimeLimit.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Recipes/TimeLimit.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -14,7 +14,7 @@
   Assume you defined the Ackermann function on the ML-level.
 *}
 
-ML{*fun ackermann (0, n) = n + 1
+ML %grayML{*fun ackermann (0, n) = n + 1
   | ackermann (m, 0) = ackermann (m - 1, 1)
   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
 
@@ -47,4 +47,4 @@
 
  
 *}
-end
\ No newline at end of file
+end

--- 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 {*

--- a/ProgTutorial/Tactical.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Tactical.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -2,14 +2,6 @@
 imports Base First_Steps
 begin
 
-(*<*)
-setup{*
-open_file_with_prelude 
-  "Tactical_Code.thy"
-  ["theory Tactical", "imports Base First_Steps", "begin"]
-*}
-(*>*)
-
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
 text {*
@@ -104,7 +96,7 @@
 
 *}
 
-ML{*val foo_tac = 
+ML %grayML{*val foo_tac = 
       (etac @{thm disjE} 1
        THEN rtac @{thm disjI2} 1
        THEN atac 1
@@ -133,7 +125,7 @@
   you can write
 *}
 
-ML{*val foo_tac' = 
+ML %grayML{*val foo_tac' = 
       (etac @{thm disjE} 
        THEN' rtac @{thm disjI2} 
        THEN' atac 
@@ -177,7 +169,7 @@
   states. Hence the type of a tactic is:
 *}
   
-ML{*type tactic = thm -> thm Seq.seq*}
+ML %grayML{*type tactic = thm -> thm Seq.seq*}
 
 text {*
   By convention, if a tactic fails, then it should return the empty sequence. 
@@ -190,14 +182,14 @@
   is defined as
 *}
 
-ML{*fun no_tac thm = Seq.empty*}
+ML %grayML{*fun no_tac thm = Seq.empty*}
 
 text {*
   which means @{ML no_tac} always fails. The second returns the given theorem wrapped 
   in a single member sequence; it is defined as
 *}
 
-ML{*fun all_tac thm = Seq.single thm*}
+ML %grayML{*fun all_tac thm = Seq.single thm*}
 
 text {*
   which means @{ML all_tac} always succeeds, but also does not make any progress 
@@ -237,7 +229,7 @@
   tactic
 *}
 
-ML{*fun my_print_tac ctxt thm =
+ML %grayML{*fun my_print_tac ctxt thm =
 let
   val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))
 in 
@@ -473,7 +465,7 @@
   explored via the lazy sequences mechanism). Given the code
 *}
 
-ML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*}
+ML %grayML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*}
 
 text {*
   an example for @{ML resolve_tac} is the following proof where first an outermost 
@@ -529,7 +521,7 @@
 \begin{isabelle}
 *}
 
-ML{*fun foc_tac {prems, params, asms, concl, context, schematics} = 
+ML %grayML{*fun foc_tac {prems, params, asms, concl, context, schematics} = 
 let 
   fun assgn1 f1 f2 xs =
     Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) 
@@ -620,7 +612,7 @@
   for example easily implement a tactic that behaves almost like @{ML atac}:
 *}
 
-ML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*}
+ML %grayML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*}
 
 text {*
   If you apply @{ML atac'} to the next lemma
@@ -982,7 +974,7 @@
   page~\pageref{tac:footacprime} can also be written as:
 *}
 
-ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, 
+ML %grayML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, 
                         atac, rtac @{thm disjI1}, atac]*}
 
 text {*
@@ -993,7 +985,7 @@
   you can also just write
 *}
 
-ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, 
+ML %grayML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, 
                        atac, rtac @{thm disjI1}, atac]*}
 
 text {*
@@ -1007,7 +999,7 @@
 
 *}
 
-ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
+ML %grayML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
 
 text {*
   will first try out whether theorem @{text disjI} applies and in case of failure 
@@ -1031,7 +1023,7 @@
   as follows:
 *}
 
-ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
+ML %grayML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
                           rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*}
 
 text {*
@@ -1074,7 +1066,7 @@
   For example:
 *}
 
-ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
+ML %grayML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
                                  rtac @{thm notI}, rtac @{thm allI}]*}
 text_raw{*\label{tac:selectprimeprime}*}
 
@@ -1127,7 +1119,7 @@
   suppose the following tactic
 *}
 
-ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
+ML %grayML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
 
 text {* which applied to the proof *}
 
@@ -1151,7 +1143,7 @@
   can implement it as
 *}
 
-ML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*}
+ML %grayML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*}
 
 text {*
   since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
@@ -1164,7 +1156,7 @@
   Supposing the tactic
 *}
 
-ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+ML %grayML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
 
 text {* 
   you can see that the following goal
@@ -1430,7 +1422,7 @@
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}*}
-ML{*fun print_ss ctxt ss =
+ML %grayML{*fun print_ss ctxt ss =
 let
   val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss
 
@@ -1471,7 +1463,7 @@
   the simplification rule @{thm [source] Diff_Int} as follows:
 *}
 
-ML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
+ML %grayML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
 
 text {*
   Printing then out the components of the simpset gives:
@@ -1488,7 +1480,7 @@
   Adding also the congruence rule @{thm [source] UN_cong} 
 *}
 
-ML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *}
+ML %grayML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *}
 
 text {*
   gives
@@ -1847,7 +1839,7 @@
   to
 *}
 
-ML{*fun fail_simproc' simpset redex = 
+ML %grayML{*fun fail_simproc' simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
   val _ = pwriteln (Pretty.block [Pretty.str "The redex:", pretty_term ctxt redex])
@@ -1863,7 +1855,7 @@
 *}
 
 
-ML{*val fail' = 
+ML %grayML{*val fail' = 
 let 
   val thy = @{theory}
   val pat = [@{term "Suc n"}]
@@ -1911,7 +1903,7 @@
 *}
 
 
-ML{*fun plus_one_simproc ss redex =
+ML %grayML{*fun plus_one_simproc ss redex =
   case redex of
     @{term "Suc 0"} => NONE
   | _ => SOME @{thm plus_one}*}
@@ -1920,7 +1912,7 @@
   and set up the simproc as follows.
 *}
 
-ML{*val plus_one =
+ML %grayML{*val plus_one =
 let
   val thy = @{theory}
   val pat = [@{term "Suc n"}] 
@@ -1958,7 +1950,7 @@
   takes a term and produces the corresponding integer value.
 *}
 
-ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
+ML %grayML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
   | dest_suc_trm t = snd (HOLogic.dest_number t)*}
 
 text {* 
@@ -1988,7 +1980,7 @@
   want to prove here, the simpset @{text "num_ss"} should suffice.
 *}
 
-ML{*fun get_thm_alt ctxt (t, n) =
+ML %grayML{*fun get_thm_alt ctxt (t, n) =
 let
   val num = HOLogic.mk_number @{typ "nat"} n
   val goal = Logic.mk_equals (t, num)
@@ -2012,7 +2004,7 @@
   theorem for the simproc.
 *}
 
-ML{*fun nat_number_simproc ss t =
+ML %grayML{*fun nat_number_simproc ss t =
 let 
   val ctxt = Simplifier.the_context ss
 in
@@ -2027,7 +2019,7 @@
   on an example, you can set it up as follows:
 *}
 
-ML{*val nat_number =
+ML %grayML{*val nat_number =
 let
   val thy = @{theory}
   val pat = [@{term "Suc n"}]
@@ -2074,7 +2066,7 @@
   and to goal states. The type of conversions is
 *}
 
-ML{*type conv = cterm -> thm*}
+ML %grayML{*type conv = cterm -> thm*}
 
 text {*
   whereby the produced theorem is always a meta-equality. A simple conversion
@@ -2312,7 +2304,7 @@
   Conv} and @{ML_ind top_conv in Conv}. For example:
 *}
 
-ML{*fun true_conj1_conv ctxt =
+ML %grayML{*fun true_conj1_conv ctxt =
 let
   val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
 in
@@ -2358,7 +2350,7 @@
   the conversion should be as follows.
 *}
 
-ML{*fun if_true1_simple_conv ctxt ctrm =
+ML %grayML{*fun if_true1_simple_conv ctxt ctrm =
   case Thm.term_of ctrm of
     Const (@{const_name If}, _) $ _ =>
       Conv.arg_conv (true_conj1_conv ctxt) ctrm
@@ -2430,7 +2422,7 @@
   Here is a tactic doing exactly that:
 *}
 
-ML{*fun true1_tac ctxt =
+ML %grayML{*fun true1_tac ctxt =
   CONVERSION 
     (Conv.params_conv ~1 (fn ctxt =>
        (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv

--- a/ProgTutorial/antiquote_setup.ML	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Mon Apr 30 14:43:52 2012 +0100
@@ -81,13 +81,13 @@
 (* checks and expression agains a result pattern *)
 fun output_response {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_pat (lhs, pat));
-     write_file_ml_blk lhs (Proof_Context.theory_of ctxt);
+     (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*)
      output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_val [] NONE lhs);
-     write_file_ml_blk lhs (Proof_Context.theory_of ctxt);
+     (*write_file_ml_blk lhs (Proof_Context.theory_of ctxt);*)
      output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)

--- a/ProgTutorial/document/root.tex	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/document/root.tex	Mon Apr 30 14:43:52 2012 +0100
@@ -100,13 +100,10 @@
 \renewcommand{\isacharverbatimopen}{}%
 \renewcommand{\isacharverbatimclose}{}}{}
 
-\isakeeptag{TutorialML}
-\renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}}
-\renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}}
+\isakeeptag{grayML}
+\renewcommand{\isataggrayML}{\begin{vanishML}\begin{graybox}}
+\renewcommand{\endisataggrayML}{\end{graybox}\end{vanishML}}
 
-\isakeeptag{TutorialMLprf}
-\renewcommand{\isatagTutorialMLprf}{\begin{grayboxwithoutsep}}
-\renewcommand{\endisatagTutorialMLprf}{\end{grayboxwithoutsep}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for code that has line numbers

Binary file progtutorial.pdf has changed