src/HOL/Tools/datatype_codegen.ML
changeset 19886 6bec6daac280
parent 19818 5c5c1208a3fa
child 20071 8f3e1ddb50e6
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Jun 14 12:11:23 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jun 14 12:12:01 2006 +0200
     1.3 @@ -10,6 +10,8 @@
     1.4    val get_datatype_spec_thms: theory -> string
     1.5      -> (((string * sort) list * (string * typ list) list) * tactic) option
     1.6    val get_all_datatype_cons: theory -> (string * string) list
     1.7 +  val add_datatype_case_const: string -> theory -> theory
     1.8 +  val add_datatype_case_defs: string -> theory -> theory
     1.9    val setup: theory -> theory
    1.10  end;
    1.11  
    1.12 @@ -353,6 +355,7 @@
    1.13      DatatypePackage.get_datatype_spec #>
    1.14    CodegenPackage.set_get_all_datatype_cons
    1.15      get_all_datatype_cons #>
    1.16 -  DatatypeHooks.add add_datatype_case_const
    1.17 +  DatatypeHooks.add add_datatype_case_const #>
    1.18 +  DatatypeHooks.add add_datatype_case_defs
    1.19  
    1.20  end;