diff -r b0b30fd6c264 -r da83a614c454 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Oct 07 16:07:16 2008 +0200
+++ b/src/HOL/Int.thy	Tue Oct 07 16:07:18 2008 +0200
@@ -1922,16 +1922,6 @@
       auto simp only: Bit0_def Bit1_def)
 
 definition
-  int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
-  [code func del]: "int_aux = of_nat_aux"
-
-lemmas int_aux_code = of_nat_aux_code [where ?'a = int, simplified int_aux_def [symmetric], code]
-
-lemma [code, code unfold, code inline del]:
-  "of_nat = (\<lambda>n. int_aux n 0)"
-  by (simp add: int_aux_def of_nat_aux_def)
-
-definition
   nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
   "nat_aux i n = nat i + n"
 
@@ -1943,7 +1933,7 @@
 lemma [code]: "nat i = nat_aux i 0"
   by (simp add: nat_aux_def)
 
-hide (open) const int_aux nat_aux
+hide (open) const nat_aux
 
 lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
   "(0\<Colon>int) = Numeral0"