# HG changeset patch
# User nipkow
# Date 1499521894 -7200
# Node ID 5be685bbd16cba13938ee51a9b0703137c3fcfcb
# Parent  6b5684ee07d9fc396b2d4504e723dd95bade4af2# Parent  2d5350c1534688d6f015328f98814b77dc74d324
merged

diff -r 6b5684ee07d9 -r 5be685bbd16c src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jul 07 16:57:50 2017 +0200
+++ b/src/HOL/List.thy	Sat Jul 08 15:51:34 2017 +0200
@@ -3216,30 +3216,14 @@
   "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
 by (induct xs) auto
 
-text \<open>Contributed by Stephan Merz:\<close>
-lemma distinct_split_list:
-  assumes "distinct (xs @ x # ys)" and "xs @ x # ys = xs' @ x # ys'"
-  shows "xs = xs'" "ys = ys'"
+lemma app_Cons_app_eqD:
+assumes "xs @ x # ys = xs' @ x # ys'" and "x \<notin> set xs" and "x \<notin> set ys"
+shows "xs = xs'" "ys = ys'"
 proof -
   show "xs = xs'"
-  proof (rule ccontr)
-    assume c: "xs \<noteq> xs'"
-    show "False"
-    proof (cases "size xs < size xs'")
-      case True
-      with assms(2) have "x \<in> set xs'"
-        by (metis in_set_conv_nth nth_append nth_append_length)
-      with assms show ?thesis by auto
-    next
-      case False
-      with c assms(2) have "size xs' < size xs"
-        by (meson append_eq_append_conv linorder_neqE_nat)
-      with assms(2) have "x \<in> set xs"
-        by (metis in_set_conv_nth nth_append nth_append_length)
-      with assms(1) show ?thesis by auto
-    qed
-  qed
-  with assms(2) show "ys = ys'" by simp
+    using assms
+    by(auto simp: append_eq_Cons_conv Cons_eq_append_conv append_eq_append_conv2)
+  with assms show "ys = ys'" by simp
 qed
 
 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"