--- 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 =