--- 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(*>*)