src/ZF/ex/data.ML

 	  ["Zero : data(A,B)",
 	   "[| a: A |] ==> One(a) : data(A,B)",
 	   "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
 	   "[| a: A; b: B;  d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
   val monos = [];
-  val type_intrs = data_typechecks
-  val type_elims = data_elims);
+  val type_intrs = datatype_intrs
+  val type_elims = datatype_elims);
 
 
 (**  Lemmas to justify using "data" in other recursive type definitions **)
 
 goalw Data.thy Data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";