--- a/src/HOL/Word/TdThs.thy	Fri Apr 24 08:24:54 2009 +0200
+++ b/src/HOL/Word/TdThs.thy	Fri Apr 24 17:45:15 2009 +0200
@@ -110,7 +110,7 @@
   done
 
 lemma fn_comm_power:
-  "fa o tr = tr o fr ==> fa o^ n o tr = tr o fr o^ n" 
+  "fa o tr = tr o fr ==> fa ^^ n o tr = tr o fr ^^ n" 
   apply (rule ext) 
   apply (induct n)
    apply (auto dest: fun_cong)