diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/Tactical.thy	Fri Feb 13 09:57:08 2009 +0000
@@ -666,7 +666,7 @@
   of the tactic is as follows.\label{tac:selecttac}
 *}
 
-ML %linenumbers{*fun select_tac (t,i) =
+ML %linenosgray{*fun select_tac (t,i) =
   case t of
      @{term "Trueprop"} $ t' => select_tac (t',i)
    | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t',i)