changeset 71 | 729fe026c5f3 |
parent 56 | 2caa6f49f06e |
--- a/src/ZF/ex/term.ML Fri Oct 22 11:34:41 1993 +0100 +++ b/src/ZF/ex/term.ML Fri Oct 22 11:42:02 1993 +0100 @@ -16,7 +16,7 @@ val ext = None val sintrs = ["[| a: A; l: list(term(A)) |] ==> Apply(a,l) : term(A)"]; val monos = [list_mono]; - val type_intrs = data_typechecks; + val type_intrs = datatype_intrs; val type_elims = [make_elim (list_univ RS subsetD)]); val [ApplyI] = Term.intrs;