--- a/src/HOL/Library/Zorn.thy Wed Jul 31 23:41:32 2013 +0200
+++ b/src/HOL/Library/Zorn.thy Thu Aug 01 00:18:45 2013 +0200
@@ -756,8 +756,7 @@
assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
shows "extension_on (Field (\<Union>R)) (\<Union>R) p"
using assms
- by (simp add: chain_subset_def extension_on_def)
- (metis Field_def mono_Field set_mp)
+ by (simp add: chain_subset_def extension_on_def) (metis mono_Field set_mp)
lemma downset_on_empty [simp]: "downset_on {} p"
by (auto simp: downset_on_def)