diff -r 02d9844ff892 -r 6f2bcdfa9a19 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/HOL.thy	Wed Jan 22 22:22:19 2025 +0100
@@ -2177,7 +2177,7 @@
     fun wrong_prem \<^Const_>\<open>All _ for \<open>Abs (_, _, t)\<close>\<close> = wrong_prem t
       | wrong_prem (Bound _) = true
       | wrong_prem _ = false;
-    val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
+    val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.take_prems_of 1);
     fun smp i = funpow i (fn m => filter_right ([spec] RL m)) [mp];
   in
     fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt];