src/ZF/ex/Prop.ML

   val sintrs = 
 	  ["Fls : prop",
 	   "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;