--- a/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy	Thu Sep 17 09:57:30 2020 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy	Thu Sep 17 09:57:31 2020 +0000
@@ -63,7 +63,7 @@
 proof (cases C)
   fix a b c d e f::word32
   assume "C = (a, b, c, d, e)"
-  thus ?thesis by (cases a) simp
+  thus ?thesis by (cases a) (simp add: take_bit_nat_eq_self)
 qed
 
 lemma steps_to_steps':