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 =