src/HOL/Induct/SList.thy

--- a/src/HOL/Induct/SList.thy	Thu Dec 15 18:13:40 2005 +0100
+++ b/src/HOL/Induct/SList.thy	Thu Dec 15 19:42:00 2005 +0100
@@ -295,9 +295,7 @@
 lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]
 
 lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
-apply (erule setup_induction)
-apply (erule list.induct, blast+)
-done
+  by (induct L == "CONS M N" set: list) auto
 
 lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
 apply (simp add: CONS_def In1_def)