src/HOL/Word/TdThs.thy

--- a/src/HOL/Word/TdThs.thy	Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Word/TdThs.thy	Mon Apr 20 09:32:07 2009 +0200
@@ -110,7 +110,7 @@
   done
 
 lemma fn_comm_power:
-  "fa o tr = tr o fr ==> fa ^ n o tr = tr o fr ^ n" 
+  "fa o tr = tr o fr ==> fa o^ n o tr = tr o fr o^ n" 
   apply (rule ext) 
   apply (induct n)
    apply (auto dest: fun_cong)