src/HOL/List.thy

--- a/src/HOL/List.thy	Sat Nov 27 17:44:36 2010 -0800
+++ b/src/HOL/List.thy	Sun Nov 28 15:20:51 2010 +0100
@@ -3625,7 +3625,7 @@
   have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
     by (auto simp:length_Suc_conv)
   then show ?case using `finite A`
-    by (auto intro: finite_imageI Suc) (* FIXME metis? *)
+    by (auto intro: Suc) (* FIXME metis? *)
 qed
 
 lemma finite_lists_length_le: