src/HOL/ZF/Zet.thy

--- a/src/HOL/ZF/Zet.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/ZF/Zet.thy	Fri May 11 00:43:45 2007 +0200
@@ -53,7 +53,7 @@
   shows "Inv A g (g x) \<in> A"
   apply (simp add: Inv_def)
   apply (rule someI2)
-  apply (auto!)
+  using `x \<in> A` apply auto
   done
 
 lemma zet_image_mem: