diff -r 3d4b49921cdb -r c346c156a7cd CookBook/Recipes/NamedThms.thy
--- a/CookBook/Recipes/NamedThms.thy	Tue Nov 25 05:19:27 2008 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Fri Nov 28 05:19:55 2008 +0100
@@ -31,29 +31,29 @@
 
   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 
+  for 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 we can declare two lemmas to be of the kind
-  @{ML_text foo}:
+  fact name @{text foo}. For example we can declare three lemmas to be of the kind
+  @{ML_text foo} by:
 *}
 
 lemma rule1[foo]: "A" sorry
 lemma rule2[foo]: "B" sorry
 lemma rule3[foo]: "C" sorry
 
-text {* undeclare them: *}
+text {* and undeclare the first one by: *}
 
 declare rule1[foo del]
 
-text {* and query them: *}
+text {* and query the remaining ones by: *}
 
 thm foo
 
 text {* 
-  In an ML-context the rules marked with @{ML_text "foo"} an be retrieved
-  using
+  On the ML-level the rules marked with @{ML_text "foo"} an be retrieved
+  using the function @{ML FooRules.get}:
 
   @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}