added hook for case const defs
authorhaftmann
Wed Jun 14 12:12:01 2006 +0200 (2006-06-14)
changeset 198866bec6daac280
parent 19885 00f70ad51778
child 19887 e3a03f1f54eb
added hook for case const defs
src/HOL/Tools/datatype_codegen.ML
     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;