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