diff -r 67cc2319104f -r 214b48a1937b src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Fri May 08 06:26:28 2020 +0000
+++ b/src/HOL/ex/Bit_Lists.thy	Fri May 08 06:26:29 2020 +0000
@@ -79,9 +79,9 @@
 lemma n_bits_of_eq_iff:
   "n_bits_of n a = n_bits_of n b \<longleftrightarrow> take_bit n a = take_bit n b"
   apply (induction n arbitrary: a b)
-   apply (auto elim!: evenE oddE simp add: take_bit_Suc)
-   apply (metis dvd_triv_right even_plus_one_iff)
-  apply (metis dvd_triv_right even_plus_one_iff)
+   apply (auto elim!: evenE oddE simp add: take_bit_Suc mod_2_eq_odd)
+    apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one)
+   apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one)
   done
 
 lemma take_n_bits_of [simp]:
@@ -98,7 +98,7 @@
 
 lemma unsigned_of_bits_n_bits_of [simp]:
   "unsigned_of_bits (n_bits_of n a) = take_bit n a"
-  by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc)
+  by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc mod_2_eq_odd)
 
 end