diff -r de51a86fc903 -r cc97b347b301 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -260,11 +260,11 @@
   fix y::int and z::int
   assume "p - (y*a) mod p = (z*a) mod p"
   then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)"
-    by (metis add_commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
+    by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
   moreover have "[y * a = (y*a) mod p] (mod p)"
     by (metis cong_int_def mod_mod_trivial)
   ultimately have "[a * (y + z) = 0] (mod p)"
-    by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult_commute ring_class.ring_distribs(1))
+    by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
   with p_prime a_nonzero p_a_relprime
   have a: "[y + z = 0] (mod p)"
     by (metis cong_prime_prod_zero_int)
@@ -319,19 +319,19 @@
 subsection {* Gauss' Lemma *}
 
 lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
-by (metis (no_types) minus_minus mult_commute mult_left_commute power_minus power_one)
+by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
 
 theorem pre_gauss_lemma:
   "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
 proof -
   have "[setprod id A = setprod id F * setprod id D](mod p)"
-    by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod.cong)
+    by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong)
   then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
     apply (rule cong_trans_int)
     apply (metis cong_scalar_int prod_F_zcong)
     done
   then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
-    by (metis C_prod_eq_D_times_E mult_commute mult_left_commute)
+    by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
   then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
     by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
   then have "[setprod id A = ((-1)^(card E) *
@@ -349,7 +349,7 @@
   then have "[setprod id A = ((-1)^(card E) * a^(card A) *
       setprod id A)](mod p)"
     apply (rule cong_trans_int)
-    apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult_assoc)
+    apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult.assoc)
     done
   then have a: "[setprod id A * (-1)^(card E) =
       ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
@@ -357,7 +357,7 @@
   then have "[setprod id A * (-1)^(card E) = setprod id A *
       (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
     apply (rule cong_trans_int)
-    apply (simp add: a mult_commute mult_left_commute)
+    apply (simp add: a mult.commute mult.left_commute)
     done
   then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)"
     apply (rule cong_trans_int)