changeset 84 | 01d6c0ddaae3 |
parent 70 | 8a29f8b4aca1 |
child 124 | 858ab9a9b047 |
--- 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;