src/ZF/ex/Enum.ML

 	  [(consts, "i")])];
   val rec_styp = "i";
   val ext = None
   val sintrs = map (fn const => const ^ " : enum") consts;
   val monos = [];
-  val type_intrs = data_typechecks
+  val type_intrs = datatype_intrs
   val type_elims = []);
 
 goal Enum.thy "con59 ~= con60";
 by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);
 result();