diff -r ef74cf118da3 -r 4426b52eabb4 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat Sep 04 22:26:48 2021 +0200
+++ b/src/Pure/more_thm.ML	Sun Sep 05 19:38:36 2021 +0200
@@ -448,15 +448,18 @@
 
 fun forall_intr_frees th =
   let
-    val fixed =
+    val fixed0 =
       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 =
-      Thm.fold_atomic_cterms (fn a =>
+    val (_, frees) =
+      (th, (fixed0, [])) |-> Thm.fold_atomic_cterms (fn a => fn (fixed, frees) =>
         (case Thm.term_of a of
-          Free v => not (Term_Subst.Frees.defined fixed v) ? insert (op aconvc) a
-        | _ => I)) th [];
+          Free v =>
+            if not (Term_Subst.Frees.defined fixed v)
+            then (Term_Subst.Frees.add (v, ()) fixed, a :: frees)
+            else (fixed, frees)
+        | _ => (fixed, frees)));
   in fold Thm.forall_intr frees th end;