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