# HG changeset patch
# User wenzelm
# Date 1753269712 -7200
# Node ID 9225b889f68ac54ccd08487ead0ab6f08de3f0a7
# Parent  cc89d72e17b85d789e6efc82308ee6a0303a84c9
more comments;

diff -r cc89d72e17b8 -r 9225b889f68a src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Wed Jul 23 13:10:34 2025 +0200
+++ b/src/Pure/term_items.ML	Wed Jul 23 13:21:52 2025 +0200
@@ -4,6 +4,7 @@
 Scalable collections of term items:
   - table: e.g. for instantiation
   - set with order of addition, e.g. occurrences within term
+    (assuming that there were no remove operations)
 *)
 
 signature TERM_ITEMS =