src/HOL/Tools/datatype_package.ML
changeset 26093 51e8d37b4e7b
parent 25888 48cc198b9ac5
child 26111 91e0999b075f
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Feb 18 21:33:29 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Feb 18 22:56:53 2008 +0100
     1.3 @@ -139,15 +139,13 @@
     1.4  
     1.5  fun the_datatype_spec thy dtco =
     1.6    let
     1.7 -    fun mk_cons typ_of_dtyp (co, tys) = (co, map typ_of_dtyp tys);
     1.8 -    fun mk_dtyp ({ sorts = raw_sorts, descr, ... } : DatatypeAux.datatype_info, (dtys, cos)) =
     1.9 -      let
    1.10 -        val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
    1.11 -          o DatatypeAux.dest_DtTFree) dtys;
    1.12 -        val typ_of_dtyp = DatatypeAux.typ_of_dtyp descr sorts;
    1.13 -        val tys = map typ_of_dtyp dtys;
    1.14 -      in (sorts, map (mk_cons typ_of_dtyp) cos) end;
    1.15 -  in mk_dtyp (the (get_datatype_descr thy dtco)) end;
    1.16 +    val info as { descr, index, sorts = raw_sorts, ... } = the_datatype thy dtco;
    1.17 +    val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
    1.18 +    val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
    1.19 +      o DatatypeAux.dest_DtTFree) dtys;
    1.20 +    val cos = map
    1.21 +      (fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
    1.22 +  in (sorts, cos) end;
    1.23  
    1.24  fun get_datatype_constrs thy dtco =
    1.25    case try (the_datatype_spec thy) dtco