tuned;

--- a/src/Pure/more_thm.ML	Mon Sep 06 12:23:06 2021 +0200
+++ b/src/Pure/more_thm.ML	Mon Sep 06 12:25:19 2021 +0200
@@ -468,17 +468,17 @@
 
 fun forall_intr_frees th =
   let
-    val fixed0 =
+    val fixed =
       Term_Subst.Frees.build
        (fold Term_Subst.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #>
         fold Term_Subst.add_frees (Thm.hyps_of th));
     val (_, frees) =
-      (th, (fixed0, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
-        (fn ct => fn (fixed, frees) =>
+      (th, (fixed, [])) |-> Thm.fold_atomic_cterms {hyps = false} Term.is_Free
+        (fn ct => fn (seen, frees) =>
           let val v = Term.dest_Free (Thm.term_of ct) in
-            if not (Term_Subst.Frees.defined fixed v)
-            then (Term_Subst.Frees.add (v, ()) fixed, ct :: frees)
-            else (fixed, frees)
+            if not (Term_Subst.Frees.defined seen v)
+            then (Term_Subst.Frees.add (v, ()) seen, ct :: frees)
+            else (seen, frees)
           end);
   in fold Thm.forall_intr frees th end;