# HG changeset patch
# User haftmann
# Date 1150279921 -7200
# Node ID 6bec6daac280d0e33599037af1c7c8a5767da624
# Parent  00f70ad51778f78c28167c5dfa2910f830cef2f9
added hook for case const defs

diff -r 00f70ad51778 -r 6bec6daac280 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Jun 14 12:11:23 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jun 14 12:12:01 2006 +0200
@@ -10,6 +10,8 @@
   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;
 
@@ -353,6 +355,7 @@
     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;