changeset 16689 05b986733a59
parent 16662 0836569a8ffc
child 16690 b8b2579a2509
--- 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