# HG changeset patch
# User wenzelm
# Date 1630925168 -7200
# Node ID a88fda85bd25c2eeffd1e2b383dfc9b307bc99c6
# Parent  5d2b87226cd1e2e248d39cfd477284e2378d3a3d
more scalable operations;

diff -r 5d2b87226cd1 -r a88fda85bd25 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Sep 06 12:25:19 2021 +0200
+++ b/src/Pure/more_thm.ML	Mon Sep 06 12:46:08 2021 +0200
@@ -463,8 +463,16 @@
 (* implicit generalization over variables -- canonical order *)
 
 fun forall_intr_vars th =
-  let val vs = build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Var (insert (op aconvc)))
-  in fold Thm.forall_intr vs th end;
+  let
+    val (_, vars) =
+      (th, (Term_Subst.Vars.empty, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Var
+        (fn ct => fn (seen, vars) =>
+          let val v = Term.dest_Var (Thm.term_of ct) in
+            if not (Term_Subst.Vars.defined seen v)
+            then (Term_Subst.Vars.add (v, ()) seen, ct :: vars)
+            else (seen, vars)
+          end);
+  in fold Thm.forall_intr vars th end;
 
 fun forall_intr_frees th =
   let