diff -r fb6c29a90003 -r d8c376662bb4 ProgTutorial/Advanced.thy
--- 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}