# HG changeset patch
# User wenzelm
# Date 1631279289 -7200
# Node ID 019fe82386568c5e085bdba6f26e7a1c76892ba8
# Parent  c2ee8d993d6a46dcdd46a6af1d9fd9885820dd6b
NEWS;

diff -r c2ee8d993d6a -r 019fe8238656 NEWS
--- a/NEWS	Fri Sep 10 14:59:19 2021 +0200
+++ b/NEWS	Fri Sep 10 15:08:09 2021 +0200
@@ -237,6 +237,17 @@
 
 *** ML ***
 
+* ML structures TFrees, TVars, Frees, Vars, Names provide scalable
+operations to accumulate items from types and terms, using a fast
+syntactic order. The original order of occurrences may be recovered as
+well, e.g. via TFrees.list_set.
+
+* Thm.instantiate, Thm.generalize and related operations require
+scalable datastructures from structure TVars, Vars, Names etc.
+INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate
+adoption; better use TVars.add, TVars.add_tfrees etc. for scalable
+accumulation of items.
+
 * ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on
 the given ML expression, in contrast to functions "try" and "can" that
 modify application of a function.