src/ZF/Datatype.ML
changeset 70 8a29f8b4aca1
parent 55 331d93292ee0
child 120 09287f26bfb8
--- 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];