--- a/ProgTutorial/Recipes/Oracle.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Recipes/Oracle.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -122,7 +122,7 @@
   To be able to use our oracle for Isar proofs, we wrap it into a tactic:
 *}
 
-ML{*val iff_oracle_tac =
+ML %grayML{*val iff_oracle_tac =
   CSUBGOAL (fn (goal, i) => 
     (case try iff_oracle goal of
       NONE => no_tac