diff -r e0938d929bfd -r 55104c664185 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Apr 22 19:16:02 2009 +0200
+++ b/src/HOL/Nat.thy	Thu Apr 23 12:17:50 2009 +0200
@@ -1220,7 +1220,7 @@
   "of_nat_aux inc 0 i = i"
   | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
 
-lemma of_nat_code [code, code unfold, code inline del]:
+lemma of_nat_code:
   "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
 proof (induct n)
   case 0 then show ?case by simp
@@ -1232,9 +1232,11 @@
     by simp
   with Suc show ?case by (simp add: add_commute)
 qed
-    
+
 end
 
+declare of_nat_code [code, code unfold, code inline del]
+
 text{*Class for unital semirings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}