diff -r 93c6f0da5c70 -r aee949f6642d src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:05 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:05 2016 +0200
@@ -510,7 +510,7 @@
       also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
         by (simp add: algebra_simps)
       finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
-    qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')
+    qed (auto simp: gcd_eucl_non_0 algebra_simps minus_mod_eq_div_mult [symmetric])
     finally show ?thesis .
   qed
 qed