diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Fri Jan 30 13:41:45 2009 +0000
+++ b/src/HOL/Algebra/IntRing.thy	Sat Jan 31 09:04:16 2009 +0100
@@ -265,6 +265,7 @@
 apply fast
 done
 
+
 lemma prime_primeideal:
   assumes prime: "prime (nat p)"
   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
@@ -293,17 +294,7 @@
 
   assume "a * b = x * p"
   hence "p dvd a * b" by simp
-  hence "nat p dvd nat (abs (a * b))"
-  apply (subst nat_dvd_iff, clarsimp)
-  apply (rule conjI, clarsimp, simp add: zabs_def)
-  proof (clarsimp)
-    assume a: " ~ 0 <= p"
-    from prime
-        have "0 < p" by (simp add: prime_def)
-    from a and this
-        have "False" by simp
-    thus "nat (abs (a * b)) = 0" ..
-  qed
+  hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
   hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
   hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
   hence "p dvd a | p dvd b" by (fast intro: unnat)