diff -r bf595bfbdc98 -r fdcc7e8f95ea src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Fri Sep 03 19:56:03 2021 +0200
+++ b/src/Pure/term_subst.ML	Sat Sep 04 13:49:26 2021 +0200
@@ -29,6 +29,15 @@
   structure TVars: INST_TABLE
   structure Frees: INST_TABLE
   structure Vars: INST_TABLE
+  val add_tfreesT: typ -> TFrees.set -> TFrees.set
+  val add_tfrees: term -> TFrees.set -> TFrees.set
+  val add_tvarsT: typ -> TVars.set -> TVars.set
+  val add_tvars: term -> TVars.set -> TVars.set
+  val add_frees: term -> Frees.set -> Frees.set
+  val add_vars: term -> Vars.set -> Vars.set
+  val add_tfree_namesT: typ -> Symtab.set -> Symtab.set
+  val add_tfree_names: term -> Symtab.set -> Symtab.set
+  val add_free_names: term -> Symtab.set -> Symtab.set
   val map_atypsT_same: typ Same.operation -> typ Same.operation
   val map_types_same: typ Same.operation -> term Same.operation
   val map_aterms_same: term Same.operation -> term Same.operation
@@ -77,6 +86,16 @@
   val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
 );
 
+val add_tfreesT = fold_atyps (fn TFree v => TFrees.add (v, ()) | _ => I);
+val add_tfrees = fold_types add_tfreesT;
+val add_tvarsT = fold_atyps (fn TVar v => TVars.add (v, ()) | _ => I);
+val add_tvars = fold_types add_tvarsT;
+val add_frees = fold_aterms (fn Free v => Frees.add (v, ()) | _ => I);
+val add_vars = fold_aterms (fn Var v => Vars.add (v, ()) | _ => I);
+val add_tfree_namesT = fold_atyps (fn TFree (a, _) => Symtab.insert_set a | _ => I);
+val add_tfree_names = fold_types add_tfree_namesT;
+val add_free_names = fold_aterms (fn Free (x, _) => Symtab.insert_set x | _ => I);
+
 
 (* generic mapping *)