Generalized nth_drop (Conny).

--- a/src/HOL/List.ML	Fri Aug 01 09:42:19 1997 +0200
+++ b/src/HOL/List.ML	Fri Aug 01 10:59:19 1997 +0200
@@ -558,7 +558,7 @@
 qed_spec_mp "nth_take";
 Addsimps [nth_take];
 
-goal thy  "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
+goal thy  "!xs i. n + i <= length xs --> nth i (drop n xs) = nth (n + i) xs";
 by (nat_ind_tac "n" 1);
  by (ALLGOALS Asm_simp_tac);
 by (rtac allI 1);