diff -r e7fb17bca374 -r 0f33c7031ec9 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Mon Apr 05 22:46:41 2021 +0200
+++ b/src/HOL/Parity.thy	Tue Apr 06 18:12:20 2021 +0000
@@ -1018,7 +1018,7 @@
     also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
       using even by (auto simp add: algebra_simps mod2_eq_if)
     finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
-      using \<open>2 * 2 ^ n \<noteq> 0\<close> by simp (simp flip: bit_Suc add: bit_double_iff)
+      using \<open>2 * 2 ^ n \<noteq> 0\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff)
     also have \<open>\<dots> \<longleftrightarrow> bit (a div 2) n \<or> bit (b div 2) n\<close>
       using bit \<open>2 ^ n \<noteq> 0\<close> by (rule Suc.IH)
     finally show ?case
@@ -1883,7 +1883,7 @@
   then show ?thesis
     apply (auto simp add: divide_int_def not_le elim!: evenE)
     apply (simp only: minus_mult_right)
-    apply (subst nat_mult_distrib)
+    apply (subst (asm) nat_mult_distrib)
      apply simp_all
     done
 qed