diff -r b933700f0384 -r 3d4953e88449 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/List.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -950,9 +950,7 @@
   proof (cases)
     assume "p x"
     hence eq: "?S' = insert 0 (Suc ` ?S)"
-      apply (auto simp add:  nth_Cons image_def neq0_conv split:nat.split elim:lessE)
-      apply (rule_tac x="xa - 1" in exI, auto)
-      done
+      by(auto simp: nth_Cons image_def split:nat.split dest:not0_implies_Suc)
     have "length (filter p (x # xs)) = Suc(card ?S)"
       using Cons `p x` by simp
     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
@@ -2460,12 +2458,7 @@
 
 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
 apply(induct xs arbitrary: I)
- apply simp
-apply(auto simp add: neq0_conv sublist_Cons nth_Cons split:nat.split elim: lessE)
- apply(erule lessE)
-  apply auto
-apply(erule lessE)
-apply auto
+apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: not0_implies_Suc)
 done
 
 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"