src/ZF/Induct/ListN.thy

--- a/src/ZF/Induct/ListN.thy	Thu Dec 15 19:42:02 2005 +0100
+++ b/src/ZF/Induct/ListN.thy	Thu Dec 15 19:42:03 2005 +0100
@@ -23,7 +23,7 @@
 
 
 lemma list_into_listn: "l \<in> list(A) ==> <length(l),l> \<in> listn(A)"
-  by (erule list.induct) (simp_all add: listn.intros)
+  by (induct set: list) (simp_all add: listn.intros)
 
 lemma listn_iff: "<n,l> \<in> listn(A) <-> l \<in> list(A) & length(l)=n"
   apply (rule iffI)