diff -r 7e54225acef1 -r 98d0f85d247f src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Mon Sep 08 23:09:37 2014 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Tue Sep 09 17:50:54 2014 +0200
@@ -3412,7 +3412,7 @@
 
     from len
       have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
-      by (simp add: drop_Suc_conv_tl)
+      by (simp add: Cons_nth_drop_Suc)
     with carr
       have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
       by simp