diff -r c3fe4749ef01 -r 83cea5dc6bac CookBook/Recipes/NamedThms.thy
--- a/CookBook/Recipes/NamedThms.thy	Wed Jan 07 16:36:31 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Thu Jan 08 22:46:06 2009 +0000
@@ -47,18 +47,21 @@
 
 declare rule1[foo del]
 
-text {* and query the remaining ones by: *}
+text {* and query the remaining ones with:
 
-thm foo
+@{ML_response_fake_both [display] "thm foo" 
+"?C
+?B"}
 
-text {* 
   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\"]"}
 
   \begin{readmore}
-  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
+  For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
+  the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
+  data.
   \end{readmore}
  *}