src/HOL/Tools/datatype_codegen.ML
changeset 18379 87cb7e641ba5
parent 18334 a41ce9c10b73
child 18386 e6240d62a7e6
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Dec 09 12:38:49 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Dec 09 15:25:29 2005 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature DATATYPE_CODEGEN =
     1.5  sig
     1.6    val is_datatype: theory -> string -> bool
     1.7 -  val get_datatype: theory -> string -> (string list * string list) option
     1.8 +  val get_datatype: theory -> string -> ((string * sort) list * string list) option
     1.9    val get_datacons: theory -> string * string -> typ list option
    1.10    val get_case_const_data: theory -> string -> (string * int) list option;
    1.11    val setup: (theory -> theory) list
    1.12 @@ -307,13 +307,11 @@
    1.13  fun get_datatype thy dtname =
    1.14    dtname
    1.15    |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    1.16 -  |> Option.map #descr
    1.17 -  |> these
    1.18 -  |> get_first (fn (_, (dtname', vs, cs)) =>
    1.19 -       if dtname = dtname'
    1.20 -       then SOME (vs, map fst cs)
    1.21 -       else NONE)
    1.22 -  |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)));
    1.23 +  |> Option.map (fn info => (#sorts info,
    1.24 +      (get_first (fn (_, (dtname', _, cs)) =>
    1.25 +        if dtname = dtname'
    1.26 +        then SOME (map fst cs)
    1.27 +        else NONE) (#descr info) |> the)));
    1.28    
    1.29  fun get_datacons thy (c, dtname) =
    1.30    let