src/HOL/Tools/datatype_codegen.ML
changeset 19599 a5c7eb37d14f
parent 19458 a70f1b0f09cd
child 19818 5c5c1208a3fa
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue May 09 10:09:17 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue May 09 10:09:37 2006 +0200
     1.3 @@ -9,9 +9,7 @@
     1.4  sig
     1.5    val get_datatype_spec_thms: theory -> string
     1.6      -> (((string * sort) list * (string * typ list) list) * tactic) option
     1.7 -  val get_case_const_data: theory -> string -> (string * int) list option
     1.8    val get_all_datatype_cons: theory -> (string * string) list
     1.9 -  val get_datatype_case_consts: theory -> string list
    1.10    val setup: theory -> theory
    1.11  end;
    1.12  
    1.13 @@ -331,17 +329,13 @@
    1.14        ((snd o the oo DatatypePackage.get_datatype_spec) thy dtco))
    1.15          (DatatypePackage.get_datatypes thy) [];
    1.16  
    1.17 -fun get_case_const_data thy c =
    1.18 -  case find_first (fn (_, {index, descr, case_name, ...}) =>
    1.19 -      case_name = c
    1.20 -    ) ((Symtab.dest o DatatypePackage.get_datatypes) thy)
    1.21 -   of NONE => NONE
    1.22 -    | SOME (_, {index, descr, ...}) =>
    1.23 -        (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
    1.24 -
    1.25 -fun get_datatype_case_consts thy =
    1.26 -  Symtab.fold (fn (_, {case_name, ...}) => cons case_name)
    1.27 -    (DatatypePackage.get_datatypes thy) [];
    1.28 +fun add_datatype_case_const dtco thy =
    1.29 +  let
    1.30 +    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco
    1.31 +  in
    1.32 +    CodegenPackage.add_case_const case_name
    1.33 +      ((map (apsnd length) o #3 o the o AList.lookup (op =) descr) index) thy
    1.34 +  end;
    1.35  
    1.36  val setup = 
    1.37    add_codegen "datatype" datatype_codegen #>
    1.38 @@ -352,8 +346,6 @@
    1.39      DatatypePackage.get_datatype_spec #>
    1.40    CodegenPackage.set_get_all_datatype_cons
    1.41      get_all_datatype_cons #>
    1.42 -  CodegenPackage.ensure_datatype_case_consts
    1.43 -    get_datatype_case_consts
    1.44 -    get_case_const_data;
    1.45 +  DatatypeHooks.add add_datatype_case_const
    1.46  
    1.47  end;