clarified signature;

--- a/src/Pure/cterm_items.ML	Thu Sep 09 15:45:27 2021 +0200
+++ b/src/Pure/cterm_items.ML	Thu Sep 09 15:55:12 2021 +0200
@@ -35,4 +35,22 @@
 end;
 
 
-structure Cterms: TERM_ITEMS = Term_Items(type key = cterm val ord = Thm.fast_term_ord);
+structure Cterms:
+sig
+  include TERM_ITEMS
+  val add_vars: thm -> set -> set
+  val add_frees: thm -> set -> set
+end =
+struct
+
+structure Term_Items = Term_Items
+(
+  type key = cterm;
+  val ord = Thm.fast_term_ord
+);
+open Term_Items;
+
+val add_vars = Thm.fold_atomic_cterms {hyps = false} Term.is_Var add_set;
+val add_frees = Thm.fold_atomic_cterms {hyps = true} Term.is_Free add_set;
+
+end;

--- a/src/Pure/more_thm.ML	Thu Sep 09 15:45:27 2021 +0200
+++ b/src/Pure/more_thm.ML	Thu Sep 09 15:55:12 2021 +0200
@@ -419,7 +419,7 @@
 (* implicit generalization over variables -- canonical order *)
 
 fun forall_intr_vars th =
-  let val vars = Cterms.build (Thm.fold_atomic_cterms {hyps = false} Term.is_Var Cterms.add_set th)
+  let val vars = Cterms.build (Cterms.add_vars th)
   in fold_rev Thm.forall_intr (Cterms.list_set vars) th end;
 
 fun forall_intr_frees th =