src/HOL/Tools/datatype_codegen.ML

 signature DATATYPE_CODEGEN =
 sig
   val get_datatype_spec_thms: theory -> string
     -> (((string * sort) list * (string * typ list) list) * tactic) option
   val get_all_datatype_cons: theory -> (string * string) list
+  val add_datatype_case_const: string -> theory -> theory
+  val add_datatype_case_defs: string -> theory -> theory
   val setup: theory -> theory
 end;
 
 structure DatatypeCodegen : DATATYPE_CODEGEN =
 struct

     get_datatype_spec_thms #>
   CodegenPackage.set_get_datatype
     DatatypePackage.get_datatype_spec #>
   CodegenPackage.set_get_all_datatype_cons
     get_all_datatype_cons #>
-  DatatypeHooks.add add_datatype_case_const
+  DatatypeHooks.add add_datatype_case_const #>
+  DatatypeHooks.add add_datatype_case_defs
 
 end;