--- a/src/HOL/MetisExamples/Abstraction.thy Fri Dec 05 11:42:27 2008 +0100
+++ b/src/HOL/MetisExamples/Abstraction.thy Fri Dec 05 15:52:12 2008 +0000
@@ -62,9 +62,9 @@
ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect"*}
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-(*???metis cannot prove this
-by (metis CollectD SigmaD1 SigmaD2 UN_eq)
-Also, UN_eq is unnecessary*)
+(*???metis says this is satisfiable!
+by (metis CollectD SigmaD1 SigmaD2)
+*)
by (meson CollectD SigmaD1 SigmaD2)