diff -r 1bfe383f69c0 -r 80ced0c233d9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Tue Feb 25 17:43:33 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Tue Feb 25 17:43:48 2025 +0100
@@ -42,18 +42,11 @@
 
 fun good_slices_of_tactic_prover name =
   (* FUDGE *)
-  if name = simpN then
-    [(1, false, false, 0, meshN),
-     (1, false, false, 2, meshN),
-     (1, false, false, 8, meshN),
-     (1, false, false, 32, meshN),
-     (1, false, false, 128, meshN)]
-  else
-    [(1, false, false, 0, meshN),
-     (1, false, false, 1, meshN),
-     (1, false, false, 2, meshN),
-     (1, false, false, 4, meshN),
-     (1, false, false, 8, meshN)]
+  [(1, false, false, 0, meshN),
+   (1, false, false, 2, meshN),
+   (1, false, false, 4, meshN),
+   (1, false, false, 8, meshN),
+   (1, false, false, 16, meshN)]
 
 (* In sync with Sledgehammer_Proof_Methods.tac_of_proof_method *)
 fun tac_of ctxt name (local_facts, global_facts) =