* Pure: structure OrdList (cf. Pure/General/ord_list.ML);
* Pure: more efficient orders for basic syntactic entities;

--- a/NEWS	Tue Jul 05 13:57:23 2005 +0200
+++ b/NEWS	Tue Jul 05 14:07:08 2005 +0200
@@ -415,6 +415,17 @@
 Poly/ML, set to 1 to profile time, 2 to profile space (which increases
 the runtime).
 
+* Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
+reasonably efficient light-weight implementation of lists as sets.
+
+* Pure: more efficient orders for basic syntactic entities: added
+fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord
+and typ_ord to use fast_string_ord and fast_indexname_ord (term_ord is
+NOT affected); structures Symtab, Vartab, Typtab, Termtab use the fast
+orders now -- potential INCOMPATIBILITY for code that depends on a
+particular order for Symtab.keys, Symtab.dest, etc. (consider using
+Library.sort_strings on result).
+
 * Pure: name spaces have been refined, with significant changes of the
 internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)
 to extern(_table).  The plain name entry path is superceded by a