test case for set_comprehension_pointfree simproc succeeds now

--- 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}