src/HOL/ex/Gauge_Integration.thy

       show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
     qed
     note rsum1 = I1[OF this]
 
     have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
-      using nth_drop'[OF `N < length D`] by simp
+      using Cons_nth_drop_Suc[OF `N < length D`] by simp
 
     have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
     proof (cases "drop (Suc N) D = []")
       case True
       note * = fine2[simplified drop_split True D_eq append_Nil2]

                simp del: append_Cons)
     qed
     note rsum2 = I2[OF this]
 
     have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
-      using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
+      using rsum_append[symmetric] Cons_nth_drop_Suc[OF `N < length D`] by auto
     also have "\<dots> = rsum D1 f + rsum D2 f"
       by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
     finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
       using add_strict_mono[OF rsum1 rsum2] by simp
   }