# 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