src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Tue Oct 30 08:45:54 2007 +0100
+++ b/src/HOL/Nat.thy	Tue Oct 30 08:45:55 2007 +0100
@@ -1289,7 +1289,7 @@
 end
 
 lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
-  by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
+  unfolding abs_if by auto
 
 lemma nat_diff_split_asm:
   "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"