src/HOL/Inductive.thy

   ("Tools/inductive_codegen.ML")
   "Tools/Datatype/datatype_aux.ML"
   "Tools/Datatype/datatype_prop.ML"
   "Tools/Datatype/datatype_case.ML"
   ("Tools/Datatype/datatype_abs_proofs.ML")
-  ("Tools/Datatype/datatype.ML")
+  ("Tools/Datatype/datatype_data.ML")
   ("Tools/old_primrec.ML")
   ("Tools/primrec.ML")
   ("Tools/Datatype/datatype_codegen.ML")
 begin
 

 subsection {* Inductive datatypes and primitive recursion *}
 
 text {* Package setup. *}
 
 use "Tools/Datatype/datatype_abs_proofs.ML"
-use "Tools/Datatype/datatype.ML"
-setup Datatype.setup
+use "Tools/Datatype/datatype_data.ML"
+setup Datatype_Data.setup
 
 use "Tools/old_primrec.ML"
 use "Tools/primrec.ML"
 
 use "Tools/Datatype/datatype_codegen.ML"

 parse_translation (advanced) {*
 let
   fun fun_tr ctxt [cs] =
     let
       val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
-      val ft = DatatypeCase.case_tr true Datatype.info_of_constr
+      val ft = DatatypeCase.case_tr true Datatype_Data.info_of_constr
                  ctxt [x, cs]
     in lambda x ft end
 in [("_lam_pats_syntax", fun_tr)] end
 *}