--- a/src/HOL/Nominal/nominal.ML Tue Jun 23 14:51:21 2009 +0200
+++ b/src/HOL/Nominal/nominal.ML Tue Jun 23 15:32:34 2009 +0200
@@ -241,13 +241,12 @@
map replace_types cargs, NoSyn)) constrs)) dts';
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
- val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
- val ((dt_names, {induction, ...}),thy1) =
+ val (full_new_type_names',thy1) =
Datatype.add_datatype config new_type_names' dts'' thy;
- val SOME {descr, ...} = Symtab.lookup
- (Datatype.get_datatypes thy1) (hd full_new_type_names');
+ val {descr, induction, ...} =
+ Datatype.the_datatype thy1 (hd full_new_type_names');
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
val big_name = space_implode "_" new_type_names;