src/ZF/list.ML
changeset 70 8a29f8b4aca1
parent 55 331d93292ee0
child 84 01d6c0ddaae3
--- a/src/ZF/list.ML	Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/list.ML	Fri Oct 22 11:34:41 1993 +0100
@@ -18,7 +18,7 @@
       ["Nil : list(A)",
        "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
   val monos = [];
-  val type_intrs = data_typechecks
+  val type_intrs = datatype_intrs
   val type_elims = []);
 
 val [NilI, ConsI] = List.intrs;