added add_hook_bootstrap
authorhaftmann
Mon Aug 14 13:46:16 2006 +0200 (2006-08-14)
changeset 2038239964c8dcd54
parent 20381 dbc1d8541bfb
child 20383 58f65fc90cf4
added add_hook_bootstrap
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Aug 14 13:46:08 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Aug 14 13:46:16 2006 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    val add_datatype_case_const: string -> theory -> theory
     1.5    val add_datatype_case_defs: string -> theory -> theory
     1.6    val datatypes_dependency: theory -> string list list
     1.7 +  val add_hook_bootstrap: DatatypeHooks.hook -> theory -> theory
     1.8    val get_datatype_mut_specs: theory -> string list
     1.9      -> ((string * sort) list * (string * (string * typ list) list) list)
    1.10    val get_datatype_arities: theory -> string list -> sort
    1.11 @@ -337,6 +338,11 @@
    1.12      |> Graph.strong_conn
    1.13    end;
    1.14  
    1.15 +fun add_hook_bootstrap hook thy =
    1.16 +  thy
    1.17 +  |> fold hook (datatypes_dependency thy)
    1.18 +  |> DatatypeHooks.add hook;
    1.19 +
    1.20  fun get_datatype_mut_specs thy (tycos as tyco :: _) =
    1.21    let
    1.22      val tycos' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
    1.23 @@ -463,8 +469,6 @@
    1.24    add_tycodegen "datatype" datatype_tycodegen #>
    1.25    CodegenTheorems.add_datatype_extr
    1.26      get_datatype_spec_thms #>
    1.27 -  CodegenPackage.set_get_all_datatype_cons
    1.28 -    get_all_datatype_cons #>
    1.29    DatatypeHooks.add (fold add_datatype_case_const) #>
    1.30    DatatypeHooks.add (fold add_datatype_case_defs)
    1.31