diff -r 1783211b3494 -r 0b55402ae95e CookBook/chunks.ML
--- a/CookBook/chunks.ML	Sat Dec 13 01:33:22 2008 +0000
+++ b/CookBook/chunks.ML	Mon Dec 15 10:48:27 2008 +0100
@@ -14,8 +14,9 @@
 );
 
 fun declare_chunk name thy =
-  (Sign.full_name thy name,
-   ChunkData.map (NameSpace.extend_table (Sign.naming_of thy) [(name, ([], stamp ()))]) thy
+  (Sign.full_bname thy name,
+   ChunkData.map (snd o NameSpace.bind (Sign.naming_of thy)
+     (Binding.name name, ([], stamp ()))) thy
    handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name));
 
 fun augment_chunk tok name =