# HG changeset patch
# User bulwahn
# Date 1508602289 -7200
# Node ID 7fe528893a6c79d70f6e17f6e201ba1125b316da
# Parent  930abfdf8727a124ea520371a017fba6b54a93cc
drop a superfluous assumption that was found by the find_unused_assms command and tune proof

diff -r 930abfdf8727 -r 7fe528893a6c src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Oct 20 20:57:55 2017 +0200
+++ b/src/HOL/List.thy	Sat Oct 21 18:11:29 2017 +0200
@@ -4902,9 +4902,8 @@
 by(induction xs arbitrary: x)(auto intro: transpD[OF assms])
 
 lemma sorted_wrt_ConsI:
-  "\<lbrakk> transp P; \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow>
-  sorted_wrt P (x # xs)"
-by (simp add: sorted_wrt_Cons)
+  "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)"
+by (induction xs rule: sorted_wrt_induct) simp_all
 
 lemma sorted_wrt_append:
 assumes "transp P"