diff -r 0d399131008f -r d50b993b4fb9 src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -665,7 +665,8 @@
   apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
   apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   apply (frule_tac a = m in pos_mod_bound)
-  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
+  apply (simp del: pos_mod_bound add: algebra_simps nat_diff_distrib gcd_diff2 nat_le_eq_zle)
+  apply (metis dual_order.strict_implies_order gcd.simps gcd_0_left gcd_diff2 mod_by_0 nat_mono)
   done
 
 lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"