src/ZF/ex/prop.ML
changeset 71 729fe026c5f3
parent 16 0b033d50ca1c
--- a/src/ZF/ex/prop.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/prop.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -24,7 +24,7 @@
 	   "n: nat ==> #n : prop",
 	   "[| p: prop;  q: prop |] ==> p=>q : prop"];
   val monos = [];
-  val type_intrs = data_typechecks;
+  val type_intrs = datatype_intrs;
   val type_elims = []);
 
 val [FlsI,VarI,ImpI] = Prop.intrs;