diff -r 01d6c0ddaae3 -r 914270f33f2d src/ZF/ex/ListN.ML
--- a/src/ZF/ex/ListN.ML	Thu Oct 28 11:30:35 1993 +0100
+++ b/src/ZF/ex/ListN.ML	Thu Oct 28 11:32:37 1993 +0100
@@ -55,4 +55,7 @@
 val listn_append = result();
 
 val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
-and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)";
+and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,l)> : listn(A)";
+
+val zero_listn_case = ListN.mk_cases List.con_defs "<0,l> : listn(A)"
+and succ_listn_case = ListN.mk_cases List.con_defs "<succ(i),l> : listn(A)";