--- a/CookBook/Recipes/NamedThms.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/Recipes/NamedThms.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -9,46 +9,53 @@
   {\bf Problem:} 
   Your tool @{text foo} works with special rules, called @{text foo}-rules.
   Users should be able to declare @{text foo}-rules in the theory,
-  which are then used by some method.\smallskip
+  which are then used in a method.\smallskip
 
-  {\bf Solution:} This can be achieved using 
+  {\bf Solution:} This can be achieved using named theorem lists.\smallskip
+
+  Named theorem lists can be set up using the code
 
   *}
+
 ML {*
-  structure FooRules = NamedThmsFun(
-    val name = "foo" 
-    val description = "Rules for foo"
-  );
+structure FooRules = NamedThmsFun (
+  val name = "foo" 
+  val description = "Rules for foo");
 *}
-
-setup FooRules.setup
+(*<*)setup FooRules.setup(*>*)
 
 text {*
+  and the command
+
+  @{ML_text [display] "setup FooRules.setup"}
+
   This code declares a context data slot where the theorems are stored,
   an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options
   to adding and deleting theorems) and an internal ML interface to retrieve and 
   modify the theorems.
 
   Furthermore, the facts are made available on the user level under the dynamic 
-  fact name @{text foo}. For example:
+  fact name @{text foo}. For example we can declare two lemmas to be of the kind
+  @{ML_text foo}:
 *}
 
 lemma rule1[foo]: "A" sorry
 lemma rule2[foo]: "B" sorry
 
+text {* undeclare them: *}
+
 declare rule1[foo del]
 
+text {* and query them: *}
+
 thm foo
 
 text {* 
   In an ML-context the rules marked with @{ML_text "foo"} an be retrieved
   using
-*}
 
-ML {* FooRules.get @{context} *}
+  @{ML_response_fake [display] "FooRules.get @{context}" "(FIXME)"}
 
-
-text {* 
   \begin{readmore}
   For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
   \end{readmore}