src/HOL/Library/Word.thy

 	hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
 	  ..
 	hence "ys ! (length ys - Suc n) = rev ys ! n"
 	  ..
 	thus "(y # ys) ! (length ys - n) = rev ys ! n"
-	  by (simp add: nth_Cons' noty not_less_iff_le [symmetric])
+	  by (simp add: nth_Cons' noty linorder_not_less [symmetric])
       next
 	assume "~ n < length ys"
 	hence x: "length ys \<le> n"
 	  by simp
 	from notx