src/ZF/ex/ListN.ML

--- a/src/ZF/ex/ListN.ML	Fri Jul 29 11:03:23 1994 +0200
+++ b/src/ZF/ex/ListN.ML	Fri Jul 29 11:09:45 1994 +0200
@@ -18,8 +18,8 @@
            "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
   val monos      = []
   val con_defs   = []
-  val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
-  val type_elims = [SigmaE2]);
+  val type_intrs = nat_typechecks @ List.intrs 
+  val type_elims = []);
 
 val listn_induct = standard 
     (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));