diff -r 5f5104069b33 -r 5d45fb978d5a src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 05 11:47:56 2014 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 05 17:06:11 2014 +0000
@@ -31,7 +31,6 @@
 imports "~~/src/HOL/GCD"
 begin
 
-declare One_nat_def [simp]
 declare [[coercion int]]
 declare [[coercion_enabled]]
 
@@ -408,9 +407,7 @@
   let ?q2 = "v * y1 + u * x2"
   from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
-    apply (auto simp add: algebra_simps) 
-    apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
-    done
+    by algebra+
   thus ?thesis by blast
 qed