src/HOL/Integ/IntDef.thy

--- a/src/HOL/Integ/IntDef.thy	Thu Jun 24 17:51:28 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu Jun 24 17:52:02 2004 +0200
@@ -503,7 +503,7 @@
 done
 
 lemma abs_int_eq [simp]: "abs (int m) = int m"
-by (simp add: zabs_def)
+by (simp add: abs_if)
 
 text{*This version is proved for all ordered rings, not just integers!
       It is proved here because attribute @{text arith_split} is not available