src/ZF/ex/enum.ML

--- a/src/ZF/ex/enum.ML	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/enum.ML	Fri Oct 22 11:42:02 1993 +0100
@@ -24,7 +24,7 @@
   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";