diff -r 065f472c09ab -r f3794c231898 CookBook/Recipes/NamedThms.thy
--- a/CookBook/Recipes/NamedThms.thy	Tue Dec 16 17:37:39 2008 +0100
+++ b/CookBook/Recipes/NamedThms.thy	Tue Dec 16 17:28:05 2008 +0000
@@ -1,5 +1,5 @@
 theory NamedThms
-imports Base
+imports "../Base"
 begin
 
 section {* Accumulate a List of Theorems under a Name *} 
@@ -27,16 +27,16 @@
 text {*
   and the command
 
-  @{ML_text [display] "setup FooRules.setup"}
+  @{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
+  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 
   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 three lemmas to be of the kind
-  @{ML_text foo} by:
+  @{text foo} by:
 *}
 
 lemma rule1[foo]: "A" sorry
@@ -52,7 +52,7 @@
 thm foo
 
 text {* 
-  On the ML-level the rules marked with @{ML_text "foo"} an be retrieved
+  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\"]"}