--- a/src/HOL/ZF/Zet.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/ZF/Zet.thy Tue Mar 02 12:26:50 2010 +0100
@@ -196,7 +196,7 @@
lemma zimage_id[simp]: "zimage id A = A"
by (simp add: zet_ext_eq zimage_iff)
-lemma zimage_cong[recdef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
+lemma zimage_cong[recdef_cong, fundef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
by (auto simp add: zet_ext_eq zimage_iff)
end