# HG changeset patch
# User lcp
# Date 751804235 -3600
# Node ID 01d6c0ddaae38d6cf58181d9a8e06e7ca384d63f
# Parent  de9316670e89f45d51f61a70a9f9159f9025e9a4
now uses datatype_intrs and datatype_elims

diff -r de9316670e89 -r 01d6c0ddaae3 src/ZF/List.ML
--- a/src/ZF/List.ML	Thu Oct 28 11:28:36 1993 +0100
+++ b/src/ZF/List.ML	Thu Oct 28 11:30:35 1993 +0100
@@ -19,7 +19,7 @@
        "[| 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;
 
diff -r de9316670e89 -r 01d6c0ddaae3 src/ZF/list.ML
--- a/src/ZF/list.ML	Thu Oct 28 11:28:36 1993 +0100
+++ b/src/ZF/list.ML	Thu Oct 28 11:30:35 1993 +0100
@@ -19,7 +19,7 @@
        "[| 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;