diff -r cd612b489504 -r 02f76f1b6e7b CookBook/Recipes/NamedThms.thy
--- a/CookBook/Recipes/NamedThms.thy	Mon Oct 27 18:48:52 2008 +0100
+++ b/CookBook/Recipes/NamedThms.thy	Wed Oct 29 13:58:36 2008 +0100
@@ -25,7 +25,7 @@
 
 text {*
   This code declares a context data slot where the theorems are stored,
-  an attribute @{attribute foo} (with the usual @{text add} and @{text del} options
+  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.
 
@@ -41,7 +41,7 @@
 thm foo
 
 text {* 
-  In an ML-context the rules marked with @{text "foo"} an be retrieved
+  In an ML-context the rules marked with @{ML_text "foo"} an be retrieved
   using
 *}