--- a/CookBook/Recipes/NamedThms.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Recipes/NamedThms.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -22,13 +22,14 @@
   val name = "foo" 
   val description = "Rules for foo");
 *}
-(*<*)setup FooRules.setup(*>*)
 
 text {*
   and the command
+*}
 
-  @{text [display] "setup FooRules.setup"}
+setup {* FooRules.setup *}
 
+text {*
   This code declares a context data slot where the theorems are stored,
   an attribute @{text foo} (with the usual @{text add} and @{text del} options
   for adding and deleting theorems) and an internal ML interface to retrieve and