--- a/src/HOL/Tools/datatype_codegen.ML Mon Aug 14 13:46:08 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Mon Aug 14 13:46:16 2006 +0200
@@ -15,6 +15,7 @@
val add_datatype_case_const: string -> theory -> theory
val add_datatype_case_defs: string -> theory -> theory
val datatypes_dependency: theory -> string list list
+ val add_hook_bootstrap: DatatypeHooks.hook -> theory -> theory
val get_datatype_mut_specs: theory -> string list
-> ((string * sort) list * (string * (string * typ list) list) list)
val get_datatype_arities: theory -> string list -> sort
@@ -337,6 +338,11 @@
|> Graph.strong_conn
end;
+fun add_hook_bootstrap hook thy =
+ thy
+ |> fold hook (datatypes_dependency thy)
+ |> DatatypeHooks.add hook;
+
fun get_datatype_mut_specs thy (tycos as tyco :: _) =
let
val tycos' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
@@ -463,8 +469,6 @@
add_tycodegen "datatype" datatype_tycodegen #>
CodegenTheorems.add_datatype_extr
get_datatype_spec_thms #>
- CodegenPackage.set_get_all_datatype_cons
- get_all_datatype_cons #>
DatatypeHooks.add (fold add_datatype_case_const) #>
DatatypeHooks.add (fold add_datatype_case_defs)