# 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