diff -r 7759f1766189 -r 50c715579715 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -626,7 +626,7 @@
       by (auto simp add: set_conv_nth)
     \<comment> "the following bound is terrible, but it simplifies the proof"
     from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
-      by (simp add: mod_add_left_eq)
+      by (simp add: mod_add_left_eq [symmetric])
     moreover
     \<comment> "why is the following so hard to prove??"
     have "\<forall>m. m < (Suc m)*(length w) + k"