--- a/NEWS Wed Dec 03 21:00:39 2008 -0800
+++ b/NEWS Thu Dec 04 14:43:33 2008 +0100
@@ -58,6 +58,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/