diff -r 04214caeb9ac -r 633fe7390c97 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Sep 08 08:41:36 2021 +0200
+++ b/src/Pure/more_thm.ML	Thu Sep 09 10:40:57 2021 +0200
@@ -218,7 +218,7 @@
   ||| list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of;
 
 
-(* tables and caches *)
+(* scalable collections *)
 
 structure Ctermtab = Table(type key = cterm val ord = fast_term_ord);
 structure Thmtab = Table(type key = thm val ord = thm_ord);