src/HOL/Nat.thy

 end
 
 text {* for code generation *}
 
 definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-  funpow_code_def [code post]: "funpow = compow"
-
-lemmas [code unfold] = funpow_code_def [symmetric]
+  funpow_code_def [code_post]: "funpow = compow"
+
+lemmas [code_unfold] = funpow_code_def [symmetric]
 
 lemma [code]:
   "funpow 0 f = id"
   "funpow (Suc n) f = f o funpow n f"
   unfolding funpow_code_def by simp_all

   with Suc show ?case by (simp add: add_commute)
 qed
 
 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.*}
 
 class semiring_char_0 = semiring_1 +