diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/NumberTheory/IntPrimes.thy
--- a/src/HOL/NumberTheory/IntPrimes.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu May 30 10:12:52 2002 +0200
@@ -264,12 +264,10 @@
 lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
   apply (frule_tac b = n and a = m in pos_mod_sign)
   apply (simp add: zgcd_def zabs_def nat_mod_distrib)
-  apply (cut_tac a = "-m" and b = n in zmod_zminus1_eq_if)
   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 add: nat_diff_distrib)
-  apply (rule gcd_diff2)
-  apply (simp add: nat_le_eq_zle)
+  apply (simp add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
+  apply (simp add: gcd_non_0 nat_mod_distrib [symmetric])
   done
 
 lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
@@ -707,7 +705,6 @@
    prefer 2
    apply (frule_tac a = "r'" in pos_mod_sign)
    apply auto
-   apply arith
   apply (rule exI)
   apply (rule exI)
   apply (subst xzgcda.simps)
@@ -727,7 +724,6 @@
    prefer 2
    apply (frule_tac a = "r'" in pos_mod_sign)
    apply auto
-   apply arith
   apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp)
   apply (subst xzgcda.simps)
   apply auto