diff -r de51a86fc903 -r cc97b347b301 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Word/Word.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -1753,7 +1753,7 @@
    prefer 2 
    apply (insert uint_range' [of s])[1]
    apply arith
-  apply (drule add_commute [THEN xtr1])
+  apply (drule add.commute [THEN xtr1])
   apply (simp add: diff_less_eq [symmetric])
   apply (drule less_le_mult)
    apply arith
@@ -2161,7 +2161,7 @@
   "a div b * b \<le> (a::nat)"
   using gt_or_eq_0 [of b]
   apply (rule disjE)
-   apply (erule xtr4 [OF thd mult_commute])
+   apply (erule xtr4 [OF thd mult.commute])
   apply clarsimp
   done
 
@@ -2921,7 +2921,7 @@
   apply (unfold shiftr_def)
   apply (induct "n")
    apply simp
-  apply (simp add: shiftr1_div_2 mult_commute
+  apply (simp add: shiftr1_div_2 mult.commute
                    zdiv_zmult2_eq [symmetric])
   done
 
@@ -2929,7 +2929,7 @@
   apply (unfold sshiftr_def)
   apply (induct "n")
    apply simp
-  apply (simp add: sshiftr1_div_2 mult_commute
+  apply (simp add: sshiftr1_div_2 mult.commute
                    zdiv_zmult2_eq [symmetric])
   done
 
@@ -3731,7 +3731,7 @@
   apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
   apply (drule bin_nth_split)
   apply safe
-       apply (simp_all add: add_commute)
+       apply (simp_all add: add.commute)
    apply (erule bin_nth_uint_imp)+
   done
 
@@ -3895,7 +3895,7 @@
 
 lemma foldl_eq_foldr:
   "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)" 
-  by (induct xs arbitrary: x) (auto simp add : add_assoc)
+  by (induct xs arbitrary: x) (auto simp add : add.assoc)
 
 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
 
@@ -3935,7 +3935,7 @@
 
 (* alternative proof of word_rcat_rsplit *)
 lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1] 
-lemmas dtle = xtr4 [OF tdle mult_commute]
+lemmas dtle = xtr4 [OF tdle mult.commute]
 
 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
   apply (rule word_eqI)
@@ -3959,7 +3959,7 @@
   fixes n::nat
   shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
   and   "(k * n + m) mod n = m mod n"
-  by (auto simp: add_commute)
+  by (auto simp: add.commute)
 
 lemma word_rsplit_rcat_size [OF refl]:
   "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow>