# HG changeset patch
# User ballarin
# Date 1212489519 -7200
# Node ID 267cab537760cd169aad80ced821bd1b40893772
# Parent  d1d35284542fbcb029a0b0ec3eb4b9303868a11e
Tuned proof.

diff -r d1d35284542f -r 267cab537760 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Tue Jun 03 12:34:22 2008 +0200
+++ b/src/HOL/Library/Zorn.thy	Tue Jun 03 12:38:39 2008 +0200
@@ -305,7 +305,7 @@
   from Zorn_Lemma2[OF this]
   obtain m B where "m:Field r" "B = r^-1 `` {m}"
     "\<forall>x\<in>Field r. B \<subseteq> r^-1 `` {x} \<longrightarrow> B = r^-1 `` {x}"
-    by(auto simp:image_def) blast
+    by auto
   hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" using po `Preorder r` `m:Field r`
     by(auto simp:subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
   thus ?thesis using `m:Field r` by blast