diff -r 4daf913fdbe1 -r 609f9ef73494 CookBook/Recipes/NamedThms.thy
--- a/CookBook/Recipes/NamedThms.thy	Thu Oct 30 13:36:51 2008 +0100
+++ b/CookBook/Recipes/NamedThms.thy	Sat Nov 01 15:20:36 2008 +0100
@@ -41,6 +41,7 @@
 
 lemma rule1[foo]: "A" sorry
 lemma rule2[foo]: "B" sorry
+lemma rule3[foo]: "C" sorry
 
 text {* undeclare them: *}
 
@@ -54,7 +55,7 @@
   In an ML-context the rules marked with @{ML_text "foo"} an be retrieved
   using
 
-  @{ML_response_fake [display] "FooRules.get @{context}" "(FIXME)"}
+  @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
 
   \begin{readmore}
   For more information see @{ML_file "Pure/Tools/named_thms.ML"}.