--- a/src/HOL/Nat.thy Thu May 14 15:09:47 2009 +0200
+++ b/src/HOL/Nat.thy Thu May 14 15:09:47 2009 +0200
@@ -1199,7 +1199,7 @@
definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
funpow_code_def [code post]: "funpow = compow"
-lemmas [code inline] = funpow_code_def [symmetric]
+lemmas [code unfold] = funpow_code_def [symmetric]
lemma [code]:
"funpow 0 f = id"
--- a/src/HOL/Power.thy Thu May 14 15:09:47 2009 +0200
+++ b/src/HOL/Power.thy Thu May 14 15:09:47 2009 +0200
@@ -452,4 +452,13 @@
from power_strict_increasing_iff [OF this] less show ?thesis ..
qed
+
+subsection {* Code generator tweak *}
+
+lemma power_power_power [code, code unfold, code inline del]:
+ "power = power.power (1::'a::{power}) (op *)"
+ unfolding power_def power.power_def ..
+
+declare power.power.simps [code]
+
end