diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Recipes/NamedThms.thy
--- a/CookBook/Recipes/NamedThms.thy	Wed Jan 14 21:46:04 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Wed Jan 14 23:44:14 2009 +0000
@@ -48,14 +48,14 @@
 
 text {* and query the remaining ones with:
 
-@{ML_response_fake_both [display] "thm foo" 
+@{ML_response_fake_both [display,gray] "thm foo" 
 "?C
 ?B"}
 
   On the ML-level the rules marked with @{text "foo"} an be retrieved
   using the function @{ML FooRules.get}:
 
-  @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
+  @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
 
   \begin{readmore}
   For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also