src/HOL/Groups_List.thy

--- a/src/HOL/Groups_List.thy	Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Groups_List.thy	Tue Apr 06 18:12:20 2021 +0000
@@ -430,7 +430,8 @@
     also have \<open>\<dots> = b # map (bit a) [0..<m]\<close>
       by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps)
     finally show ?thesis
-      using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps mod_2_eq_odd)
+      using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps)
+        (simp_all add: ac_simps mod_2_eq_odd)
   qed
 qed