1.1 --- a/src/HOL/Library/Permutations.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Library/Permutations.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -1033,7 +1033,7 @@
     1.4          by simp
     1.5        then have bc: "b = c"
     1.6          by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def
     1.7 -            cong del: if_weak_cong split: split_if_asm)
     1.8 +            cong del: if_weak_cong split: if_split_asm)
     1.9        from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) =
    1.10          (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp
    1.11        then have "p = q"