src/ZF/ex/LList.ML

   val ext = None
   val sintrs = 
       ["LNil : llist(A)",
        "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   val monos = [];
-  val type_intrs = co_data_typechecks
+  val type_intrs = co_datatype_intrs
   val type_elims = []);
   
 val [LNilI, LConsI] = LList.intrs;
 
 (*An elimination rule, for type-checking*)

  [Transset_quniv, QPair_Int_quniv_in_quniv, Int_Vfrom_0_in_quniv, 
   zero_Int_in_quniv, one_Int_in_quniv,
   QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
 
 val quniv_cs = ZF_cs addSIs in_quniv_rls 
-                     addIs (Int_quniv_in_quniv::co_data_typechecks);
+                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
 
 (*Keep unfolding the lazy list until the induction hypothesis applies*)
 goal LList.thy
    "!!i. i : nat ==> 	\
 \        ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)";