src/Pure/term_items.ML

--- a/src/Pure/term_items.ML	Sun Dec 31 22:39:40 2023 +0100
+++ b/src/Pure/term_items.ML	Mon Jan 01 14:36:08 2024 +0100
@@ -222,4 +222,16 @@
 end;
 
 
-structure Types = Term_Items(type key = typ val ord = Term_Ord.typ_ord);
+structure Types:
+sig
+  include TERM_ITEMS
+  val add_atyps: term -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items(type key = typ val ord = Term_Ord.typ_ord);
+open Term_Items;
+
+val add_atyps = (fold_types o fold_atyps) add_set;
+
+end;