diff -r 2230b7047376 -r 9a5f43dac883 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Word/Word.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -1416,7 +1416,7 @@
   apply (unfold udvd_def)
   apply safe
    apply (simp add: unat_def nat_mult_distrib)
-  apply (simp add: uint_nat int_mult)
+  apply (simp add: uint_nat of_nat_mult)
   apply (rule exI)
   apply safe
    prefer 2
@@ -3295,7 +3295,7 @@
   apply (unfold dvd_def) 
   apply auto 
   apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
-  apply (simp add : int_mult of_nat_power)
+  apply (simp add : of_nat_mult of_nat_power)
   apply (simp add : nat_mult_distrib nat_power_eq)
   done
 
@@ -4240,9 +4240,10 @@
   apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
   apply (rule rotater_eqs)
   apply (simp add: word_size nat_mod_distrib)
-  apply (rule int_eq_0_conv [THEN iffD1])
-  apply (simp only: zmod_int of_nat_add)
-  apply (simp add: rdmods)
+  apply (rule of_nat_eq_0_iff [THEN iffD1])
+  apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
+  using mod_mod_trivial zmod_eq_dvd_iff
+  apply blast
   done
 
 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]