diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Library/Permutation.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -211,7 +211,7 @@
     proof (rule bij_betw_combine)
       show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
         using bij unfolding bij_betw_def
-        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
+        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def)
     qed (auto simp: bij_betw_def)
     fix i
     assume "i < length (z#xs)"