--- a/NEWS Sat Nov 20 12:53:18 2021 +0100
+++ b/NEWS Sat Nov 20 12:59:53 2021 +0100
@@ -390,11 +390,11 @@
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.
+* Thm.instantiate, Thm.generalize and related operations (e.g.
+Variable.import) now use scalable data structures 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.
* Thm.instantiate_beta applies newly emerging abstractions to their
arguments in the term, but leaves other beta-redexes unchanged --- in