diff -r 541e68d1a964 -r 67cc2319104f src/HOL/String.thy
--- a/src/HOL/String.thy	Fri May 08 06:26:27 2020 +0000
+++ b/src/HOL/String.thy	Fri May 08 06:26:28 2020 +0000
@@ -90,7 +90,7 @@
     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)
+      using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps mod_2_eq_odd)
   qed
 qed