src/HOL/Nominal/nominal.ML
changeset 31783 cfbe9609ceb1
parent 31781 861e675f01e6
child 31784 bd3486c57ba3
     1.1 --- a/src/HOL/Nominal/nominal.ML	Tue Jun 23 14:51:21 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal.ML	Tue Jun 23 15:32:34 2009 +0200
     1.3 @@ -241,13 +241,12 @@
     1.4          map replace_types cargs, NoSyn)) constrs)) dts';
     1.5  
     1.6      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
     1.7 -    val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
     1.8  
     1.9 -    val ((dt_names, {induction, ...}),thy1) =
    1.10 +    val (full_new_type_names',thy1) =
    1.11        Datatype.add_datatype config new_type_names' dts'' thy;
    1.12  
    1.13 -    val SOME {descr, ...} = Symtab.lookup
    1.14 -      (Datatype.get_datatypes thy1) (hd full_new_type_names');
    1.15 +    val {descr, induction, ...} =
    1.16 +      Datatype.the_datatype thy1 (hd full_new_type_names');
    1.17      fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
    1.18  
    1.19      val big_name = space_implode "_" new_type_names;