# HG changeset patch # User haftmann # Date 1134138329 -3600 # Node ID 87cb7e641ba5d52421d2885d350169c5aafeeaea # Parent 35fba71ec6ef550178e5f5e44d95d96c6f36eae6 improved extraction interface diff -r 35fba71ec6ef -r 87cb7e641ba5 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Fri Dec 09 12:38:49 2005 +0100 +++ b/src/HOL/Tools/datatype_codegen.ML Fri Dec 09 15:25:29 2005 +0100 @@ -8,7 +8,7 @@ signature DATATYPE_CODEGEN = sig val is_datatype: theory -> string -> bool - val get_datatype: theory -> string -> (string list * string list) option + val get_datatype: theory -> string -> ((string * sort) list * string list) option val get_datacons: theory -> string * string -> typ list option val get_case_const_data: theory -> string -> (string * int) list option; val setup: (theory -> theory) list @@ -307,13 +307,11 @@ fun get_datatype thy dtname = dtname |> Symtab.lookup (DatatypePackage.get_datatypes thy) - |> Option.map #descr - |> these - |> get_first (fn (_, (dtname', vs, cs)) => - if dtname = dtname' - then SOME (vs, map fst cs) - else NONE) - |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree))); + |> Option.map (fn info => (#sorts info, + (get_first (fn (_, (dtname', _, cs)) => + if dtname = dtname' + then SOME (map fst cs) + else NONE) (#descr info) |> the))); fun get_datacons thy (c, dtname) = let