src/ZF/datatype.ML

--- a/src/ZF/datatype.ML	Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/datatype.ML	Fri Oct 22 11:34:41 1993 +0100
@@ -52,19 +52,19 @@
 
 
 (*For most datatypes involving univ*)
-val data_typechecks = 
+val datatype_intrs = 
     [SigmaI, InlI, InrI,
      Pair_in_univ, Inl_in_univ, Inr_in_univ, 
      zero_in_univ, A_into_univ, nat_into_univ, UnCI];
 
 (*Needed for mutual recursion*)
-val data_elims = [make_elim InlD, make_elim InrD];
+val datatype_elims = [make_elim InlD, make_elim InrD];
 
 (*For most co-datatypes involving quniv*)
-val co_data_typechecks = 
+val co_datatype_intrs = 
     [QSigmaI, QInlI, QInrI,
      QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
      zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
 
-val co_data_elims = [make_elim QInlD, make_elim QInrD];
+val co_datatype_elims = [make_elim QInlD, make_elim QInrD];