# HG changeset patch
# User haftmann
# Date 1232611738 -3600
# Node ID e8c121c644750e89d265842be095780c9e90ec07
# Parent  24a58ae5dc0e4879e86931b18d01be711160f2af
binding replaces Binding.T

diff -r 24a58ae5dc0e -r e8c121c64475 NEWS
--- a/NEWS	Thu Jan 22 09:04:56 2009 +0100
+++ b/NEWS	Thu Jan 22 09:08:58 2009 +0100
@@ -72,13 +72,13 @@
 
     class foo = ...     instead of      class foo = type + ...
 
-* Type Binding.T gradually replaces formerly used type bstring for names
+* Type binding 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
+    -> binding -> NameSpace.T -> string * NameSpace.T
   NameSpace.bind: NameSpace.naming
-    -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
+    -> binding * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
          (*exception Symtab.DUP*)
 
 See further modules src/Pure/General/binding.ML and