# HG changeset patch
# User wenzelm
# Date 1631195712 -7200
# Node ID 64be5f22446286b13b9cbd87108663f7b0a22077
# Parent  ad2899cdd52801429013e89491c94134183a348b
clarified signature;

diff -r ad2899cdd528 -r 64be5f224462 src/Pure/cterm_items.ML
--- 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;
diff -r ad2899cdd528 -r 64be5f224462 src/Pure/more_thm.ML
--- 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 =