--- a/src/HOL/Tools/datatype_codegen.ML Thu Jun 28 19:09:34 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Jun 28 19:09:35 2007 +0200
@@ -11,8 +11,6 @@
val get_eq_datatype: theory -> string -> thm list
val dest_case_expr: theory -> term
-> ((string * typ) list * ((term * typ) * (term * term) list)) option
- val add_datatype_case_const: string -> theory -> theory
- val add_datatype_case_defs: string -> theory -> theory
type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
-> theory -> theory
@@ -408,19 +406,6 @@
end;
-fun add_datatype_case_const dtco thy =
- let
- val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
- in
- CodegenPackage.add_appconst (case_name, CodegenPackage.appgen_case dest_case_expr) thy
- end;
-
-fun add_datatype_case_defs dtco thy =
- let
- val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
- in
- fold_rev (CodegenData.add_func true) case_rewrites thy
- end;
(** codetypes for code 2nd generation **)
@@ -596,6 +581,20 @@
(** theory setup **)
+fun add_datatype_case_const dtco thy =
+ let
+ val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
+ in
+ CodegenPackage.add_appconst (case_name, CodegenPackage.appgen_case dest_case_expr) thy
+ end;
+
+fun add_datatype_case_defs dtco thy =
+ let
+ val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
+ in
+ fold_rev (CodegenData.add_func true) case_rewrites thy
+ end;
+
val setup =
add_codegen "datatype" datatype_codegen
#> add_tycodegen "datatype" datatype_tycodegen