--- a/ProgTutorial/Recipes/TimeLimit.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Recipes/TimeLimit.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -14,7 +14,7 @@
   Assume you defined the Ackermann function on the ML-level.
 *}
 
-ML{*fun ackermann (0, n) = n + 1
+ML %grayML{*fun ackermann (0, n) = n + 1
   | ackermann (m, 0) = ackermann (m - 1, 1)
   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
 
@@ -47,4 +47,4 @@
 
  
 *}
-end
\ No newline at end of file
+end