# HG changeset patch
# User haftmann
# Date 1203371813 -3600
# Node ID 51e8d37b4e7bb4b49cc984f322c7503326873d60
# Parent  260cca2e16fa755ed8417d5a08cc39f06e686720
tuned

diff -r 260cca2e16fa -r 51e8d37b4e7b src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Feb 18 21:33:29 2008 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Mon Feb 18 22:56:53 2008 +0100
@@ -139,15 +139,13 @@
 
 fun the_datatype_spec thy dtco =
   let
-    fun mk_cons typ_of_dtyp (co, tys) = (co, map typ_of_dtyp tys);
-    fun mk_dtyp ({ sorts = raw_sorts, descr, ... } : DatatypeAux.datatype_info, (dtys, cos)) =
-      let
-        val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
-          o DatatypeAux.dest_DtTFree) dtys;
-        val typ_of_dtyp = DatatypeAux.typ_of_dtyp descr sorts;
-        val tys = map typ_of_dtyp dtys;
-      in (sorts, map (mk_cons typ_of_dtyp) cos) end;
-  in mk_dtyp (the (get_datatype_descr thy dtco)) end;
+    val info as { descr, index, sorts = raw_sorts, ... } = the_datatype thy dtco;
+    val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
+    val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
+      o DatatypeAux.dest_DtTFree) dtys;
+    val cos = map
+      (fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
+  in (sorts, cos) end;
 
 fun get_datatype_constrs thy dtco =
   case try (the_datatype_spec thy) dtco