diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/Recipes/Oracle.thy
--- a/ProgTutorial/Recipes/Oracle.thy	Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/Recipes/Oracle.thy	Mon Aug 27 10:24:10 2012 +0100
@@ -57,7 +57,7 @@
   the string, we use functions from the @{text Buffer} module.
   *}
 
-ML {*fun translate t =
+ML %grayML{*fun translate t =
   let
     fun trans t =
       (case t of
@@ -72,8 +72,7 @@
          Buffer.add n #>
          Buffer.add " "
       | _ => error "inacceptable term")
-  in Buffer.content (trans t Buffer.empty) end
-*}
+  in Buffer.content (trans t Buffer.empty) end*}
 
 text {*
   Here is the string representation of the term @{term "p = (q = p)"}: