--- 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)"