src/HOL/List.thy

--- a/src/HOL/List.thy	Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/List.thy	Tue Apr 20 17:58:34 2010 +0200
@@ -3039,6 +3039,9 @@
 lemma length_replicate [simp]: "length (replicate n x) = n"
 by (induct n) auto
 
+lemma Ex_list_of_length: "\<exists>xs. length xs = n"
+by (rule exI[of _ "replicate n undefined"]) simp
+
 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
 by (induct n) auto