1.1 --- a/doc-src/Inductive/ind-defs.tex	Tue Jan 19 11:16:39 1999 +0100
     1.2 +++ b/doc-src/Inductive/ind-defs.tex	Tue Jan 19 11:18:11 1999 +0100
     1.3 @@ -632,9 +632,9 @@
     1.4  deduces the corresponding form of~$i$;  this is called rule inversion.  
     1.5  Here is a sample session: 
     1.6  \begin{ttbox}
     1.7 -listn.mk_cases list.con_defs "<i,Nil> : listn(A)";
     1.8 +listn.mk_cases "<i,Nil> : listn(A)";
     1.9  {\out "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm}
    1.10 -listn.mk_cases list.con_defs "<i,Cons(a,l)> : listn(A)";
    1.11 +listn.mk_cases "<i,Cons(a,l)> : listn(A)";
    1.12  {\out "[| <?i, Cons(?a, ?l)> : listn(?A);}
    1.13  {\out     !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q }
    1.14  {\out  |] ==> ?Q" : thm}