diff -r 0fdabe28f0e6 -r 93d78fdeb55a src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Mon Aug 20 19:52:24 2007 +0200
+++ b/src/HOL/IntDef.thy	Mon Aug 20 19:52:52 2007 +0200
@@ -682,9 +682,4 @@
 where
   "int \<equiv> of_nat"
 
-abbreviation
-  int_of_nat :: "nat \<Rightarrow> int"
-where
-  "int_of_nat \<equiv> of_nat"
-
 end