src/HOL/Library/Permutations.thy
changeset 62390 842917225d56
parent 61424 c3658c18b7bc
child 63099 af0e964aad7b
--- a/src/HOL/Library/Permutations.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Library/Permutations.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -1033,7 +1033,7 @@
         by simp
       then have bc: "b = c"
         by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def
-            cong del: if_weak_cong split: split_if_asm)
+            cong del: if_weak_cong split: if_split_asm)
       from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) =
         (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp
       then have "p = q"