# HG changeset patch
# User bulwahn
# Date 1329382294 -3600
# Node ID fe51817749d190b8685f9c5b0cf92f98869aefc3
# Parent  0196966d6d2d42d8b07c8cfa3aa71772ae4a0ab8
simplifying proof

diff -r 0196966d6d2d -r fe51817749d1 src/HOL/ex/Gauge_Integration.thy
--- a/src/HOL/ex/Gauge_Integration.thy	Thu Feb 16 09:18:23 2012 +0100
+++ b/src/HOL/ex/Gauge_Integration.thy	Thu Feb 16 09:51:34 2012 +0100
@@ -417,8 +417,7 @@
     def D1 \<equiv> "take N D @ [(d, t, b)]"
     def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
 
-    have "D \<noteq> []" using `N < length D` by auto
-    from hd_drop_conv_nth[OF this `N < length D`]
+    from hd_drop_conv_nth[OF `N < length D`]
     have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
     with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
     have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"