src/ZF/List.ML

   val sintrs = 
       ["Nil : list(A)",
        "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
   val monos = [];
   val type_intrs = datatype_intrs
-  val type_elims = []);
+  val type_elims = datatype_elims);
 
 val [NilI, ConsI] = List.intrs;
 
 (*An elimination rule, for type-checking*)
 val ConsE = List.mk_cases List.con_defs "Cons(a,l) : list(A)";