diff -r de0d280c31a7 -r 2c7a24f74db9 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Nat.thy	Tue Jul 14 10:54:04 2009 +0200
@@ -1200,9 +1200,9 @@
 text {* for code generation *}
 
 definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-  funpow_code_def [code post]: "funpow = compow"
+  funpow_code_def [code_post]: "funpow = compow"
 
-lemmas [code unfold] = funpow_code_def [symmetric]
+lemmas [code_unfold] = funpow_code_def [symmetric]
 
 lemma [code]:
   "funpow 0 f = id"
@@ -1265,7 +1265,7 @@
 
 end
 
-declare of_nat_code [code, code unfold, code inline del]
+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.*}