diff -r e6fdcaaadbd3 -r dd46786d4f95 src/HOL/Relation_Power.thy
--- a/src/HOL/Relation_Power.thy	Tue Oct 07 16:07:21 2008 +0200
+++ b/src/HOL/Relation_Power.thy	Tue Oct 07 16:07:22 2008 +0200
@@ -54,7 +54,7 @@
   "fun_pow 0 f = id"
   | "fun_pow (Suc n) f = f o fun_pow n f"
 
-lemma funpow_fun_pow [code inline]: "f ^ n = fun_pow n f"
+lemma funpow_fun_pow [code unfold]: "f ^ n = fun_pow n f"
   unfolding funpow_def fun_pow_def ..
 
 lemma funpow_add: "f ^ (m+n) = f^m o f^n"