diff -r b9eb9c2b87c7 -r 65318db3087b src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 10 10:47:52 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Wed Oct 10 10:48:17 2012 +0200
@@ -60,10 +60,8 @@
   by simp
 
 lemma
-  "finite {s'. EX s:S. s' = f a e s}"
-  unfolding Bex_def
-  apply simp
-  oops
+  "finite S ==> finite {s'. EX s:S. s' = f a e s}"
+  by simp
 
 schematic_lemma (* check interaction with schematics *)
   "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}