src/HOL/Inductive.thy

   ("Tools/datatype_prop.ML")
   ("Tools/datatype_rep_proofs.ML")
   ("Tools/datatype_abs_proofs.ML")
   ("Tools/datatype_case.ML")
   ("Tools/datatype_package.ML")
-  ("Tools/datatype_codegen.ML")
   ("Tools/primrec_package.ML")
 begin
 
 subsection {* Inductive predicates and sets *}
 

 use "Tools/datatype_abs_proofs.ML"
 use "Tools/datatype_case.ML"
 use "Tools/datatype_package.ML"
 setup DatatypePackage.setup
 use "Tools/primrec_package.ML"
-use "Tools/datatype_codegen.ML"
-setup DatatypeCodegen.setup
 
 use "Tools/inductive_codegen.ML"
 setup InductiveCodegen.setup
 
 text{* Lambda-abstractions with pattern matching: *}