--- a/NEWS Thu Dec 04 14:17:36 2008 +0100
+++ b/NEWS Thu Dec 04 14:44:07 2008 +0100
@@ -61,6 +61,18 @@
*** Pure ***
+* Type Binding.T gradually replaces formerly used type bstring for names
+to be bound. Name space interface for declarations has been simplified:
+
+ NameSpace.declare: NameSpace.naming
+ -> Binding.T -> NameSpace.T -> string * NameSpace.T
+ NameSpace.bind: NameSpace.naming
+ -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
+ (*exception Symtab.DUP*)
+
+See further modules src/Pure/General/binding.ML and
+src/Pure/General/name_space.ML
+
* Module moves in repository:
src/Pure/Tools/value.ML ~> src/Tools/
src/Pure/Tools/quickcheck.ML ~> src/Tools/