src/ZF/func.thy

--- a/src/ZF/func.thy	Thu Nov 07 16:03:26 2019 +0100
+++ b/src/ZF/func.thy	Fri Nov 08 12:07:39 2019 +0100
@@ -356,8 +356,8 @@
 apply (blast intro!: rel_Union function_Union)
 done
 
-lemma gen_relation_Union [rule_format]:
-     "\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(\<Union>(F))"
+lemma gen_relation_Union:
+     "(\<And>f. f\<in>F \<Longrightarrow> relation(f)) \<Longrightarrow> relation(\<Union>(F))"
 by (simp add: relation_def)