--- a/src/HOL/Word/Word_Examples.thy Sat Jul 04 20:45:21 2020 +0000
+++ b/src/HOL/Word/Word_Examples.thy Sat Jul 04 20:45:24 2020 +0000
@@ -81,7 +81,8 @@
lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
text "this is not exactly fast, but bearable"
-lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
+lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
+ by (simp add: numeral_eq_Suc)
text "this works only for replicate n True"
lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"