src/HOL/List.thy

--- a/src/HOL/List.thy	Fri May 06 20:25:41 2011 +0200
+++ b/src/HOL/List.thy	Mon May 09 12:26:25 2011 +0200
@@ -1814,7 +1814,7 @@
 done
 
 lemma take_add: 
-  "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
+  "take (i+j) xs = take i xs @ take j (drop i xs)"
 apply (induct xs arbitrary: i, auto) 
 apply (case_tac i, simp_all)
 done