src/ZF/ex/Comb.ML

   val sintrs = 
 	  ["K : comb",
 	   "S : comb",
 	   "[| p: comb;  q: comb |] ==> p#q : comb"];
   val monos = [];
-  val type_intrs = data_typechecks;
+  val type_intrs = datatype_intrs;
   val type_elims = []);
 
 val [K_comb,S_comb,Ap_comb] = Comb.intrs;
 
 val Ap_E = Comb.mk_cases Comb.con_defs "p#q : comb";