--- 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 *)