update NEWS: Sortset and Termset turned out to be counter productive, Ord_List.union is much lighter;

--- a/NEWS	Tue Apr 18 19:11:05 2023 +0200
+++ b/NEWS	Tue Apr 18 20:54:25 2023 +0200
@@ -295,12 +295,6 @@
   - The new "size" operation works with constant time complexity and
     minimal space overhead: small structures have no size descriptor.
 
-  - Various internal interfaces now use scalable Set() instances instead
-    of plain list, notably Thm.hyps_of and Thm.shyps_of. Minor
-    INCOMPATIBILITY: use e.g. Termset.dest to adapt the result, better
-    use proper Termset operations such as Termset.exists or Termset.fold
-    without the overhead of destruction.
-
 * Operations ML_Heap.sizeof1 and ML_Heap.sizeof determine the object
 size on the heap in bytes. The latter works simultaneously on multiple
 objects, taking implicit sharing of values into account. Examples for