diff -r 7759f1766189 -r 50c715579715 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -40,7 +40,7 @@
   apply (insert m_gt_one)
   apply (rule abelian_groupI)
   apply (unfold R_def residue_ring_def)
-  apply (auto simp add: mod_add_right_eq [symmetric] ac_simps)
+  apply (auto simp add: mod_add_right_eq ac_simps)
   apply (case_tac "x = 0")
   apply force
   apply (subgoal_tac "(x + (m - x)) mod m = 0")
@@ -55,7 +55,7 @@
   apply auto
   apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
   apply (erule ssubst)
-  apply (subst mod_mult_right_eq [symmetric])+
+  apply (subst mod_mult_right_eq)+
   apply (simp_all only: ac_simps)
   done
 
@@ -64,9 +64,9 @@
   apply (rule abelian_group)
   apply (rule comm_monoid)
   apply (unfold R_def residue_ring_def, auto)
-  apply (subst mod_add_eq [symmetric])
+  apply (subst mod_add_eq)
   apply (subst mult.commute)
-  apply (subst mod_mult_right_eq [symmetric])
+  apply (subst mod_mult_right_eq)
   apply (simp add: field_simps)
   done
 
@@ -116,9 +116,9 @@
   apply auto
   apply (rule the_equality)
   apply auto
-  apply (subst mod_add_right_eq [symmetric])
+  apply (subst mod_add_right_eq)
   apply auto
-  apply (subst mod_add_left_eq [symmetric])
+  apply (subst mod_add_left_eq)
   apply auto
   apply (subgoal_tac "y mod m = - x mod m")
   apply simp
@@ -143,13 +143,11 @@
 
 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
   unfolding R_def residue_ring_def
-  apply auto
-  apply presburger
-  done
+  by (auto simp add: mod_simps)
 
 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
   unfolding R_def residue_ring_def
-  by auto (metis mod_mult_eq)
+  by (auto simp add: mod_simps)
 
 lemma zero_cong: "\<zero> = 0"
   unfolding R_def residue_ring_def by auto