diff -r 7e54225acef1 -r 98d0f85d247f src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Sep 08 23:09:37 2014 +0200
+++ b/src/HOL/List.thy	Tue Sep 09 17:50:54 2014 +0200
@@ -2009,7 +2009,7 @@
 apply (case_tac i, auto)
 done
 
-lemma drop_Suc_conv_tl:
+lemma Cons_nth_drop_Suc:
   "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
 apply (induct xs arbitrary: i, simp)
 apply (case_tac i, auto)
@@ -2200,16 +2200,6 @@
   finally show ?thesis .
 qed
 
-lemma nth_drop':
-  "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
-apply (induct i arbitrary: xs)
-apply (simp add: neq_Nil_conv)
-apply (erule exE)+
-apply simp
-apply (case_tac xs)
-apply simp_all
-done
-
 
 subsubsection {* @{const takeWhile} and @{const dropWhile} *}
 
@@ -5264,9 +5254,9 @@
   apply (rule_tac x ="x ! i" in exI) 
   apply (rule_tac x ="y ! i" in exI, safe) 
   apply (rule_tac x="drop (Suc i) x" in exI)
-  apply (drule sym, simp add: drop_Suc_conv_tl) 
+  apply (drule sym, simp add: Cons_nth_drop_Suc) 
   apply (rule_tac x="drop (Suc i) y" in exI)
-  by (simp add: drop_Suc_conv_tl) 
+  by (simp add: Cons_nth_drop_Suc) 
 
 -- {* lexord is extension of partial ordering List.lex *} 
 lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"