* Name bindings in higher specification mechanisms (notably
LocalTheory.define, LocalTheory.note, and derived packages) are now
formalized as type Name.binding, replacing old bstring.
INCOMPATIBILITY, need to wrap strings via Name.binding function, see
also Name.name_of.  Packages should pass name bindings given by the
user to underlying specification mechanisms; this enables precise
tracking of source positions, for example.

Reply via email to