src/HOL/Library/Formal_Power_Series.thy

--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Jun 23 12:09:30 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Jun 23 14:24:58 2009 +0200
@@ -1204,10 +1204,6 @@
     apply simp
     unfolding One_nat_def[symmetric] natlist_trivial_1
     apply simp
-    unfolding image_Collect[symmetric]
-    unfolding Collect_def mem_def
-    apply (rule finite_imageI)
-    apply blast
     done
 qed