diff -r fc19de122712 -r 8a48e18f081e src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Sat Oct 01 07:56:53 2022 +0000
@@ -108,7 +108,7 @@
 
 
 lemma iter_unroll: "0 < length w \<Longrightarrow> w\<^sup>\<omega> = w \<frown> w\<^sup>\<omega>"
-  by (rule ext) (simp add: conc_def mod_geq)
+  by (simp add: fun_eq_iff mod_if)
 
 
 subsection \<open>Subsequence, Prefix, and Suffix\<close>