# HG changeset patch
# User bulwahn
# Date 1508602616 -7200
# Node ID 5ec8cd4db7e2465b4b96988fb16245949885fe5f
# Parent  e92d48a42a01a663cf2e01c3a988eac13b4353e9
drop a superfluous assumption that was found by the find_unused_assms command

diff -r e92d48a42a01 -r 5ec8cd4db7e2 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Oct 21 18:14:59 2017 +0200
+++ b/src/HOL/List.thy	Sat Oct 21 18:16:56 2017 +0200
@@ -2259,7 +2259,7 @@
   finally show ?thesis .
 qed
 
-lemma take_update_swap: "n < m \<Longrightarrow> take m (xs[n := x]) = (take m xs)[n := x]"
+lemma take_update_swap: "take m (xs[n := x]) = (take m xs)[n := x]"
 apply(cases "n \<ge> length xs")
  apply simp
 apply(simp add: upd_conv_take_nth_drop take_Cons drop_take min_def diff_Suc