diff -r 2bc2a8599369 -r a03a63b81f44 src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/ZF/Zet.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -37,7 +37,7 @@
   apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
   apply (simp add: explode_Repl_eq)
   apply (subgoal_tac "explode z = f ` A")
-  apply (simp_all add: image_comp [symmetric])
+  apply (simp_all add: image_image cong: image_cong_simp)
   done
 
 lemma zet_image_mem:
@@ -98,7 +98,7 @@
 lemma zimplode_zexplode: "zimplode (zexplode z) = z"
   apply (simp add: zimplode_def zexplode_def)
   apply (subst Abs_zet_inverse)
-  apply (auto simp add: explode_mem_zet implode_explode)
+  apply (auto simp add: explode_mem_zet)
   done  
 
 lemma zin_zexplode_eq: "zin x (zexplode A) = Elem x A"