diff -r cfbe9609ceb1 -r bd3486c57ba3 src/HOL/Nominal/nominal.ML
--- a/src/HOL/Nominal/nominal.ML	Tue Jun 23 15:32:34 2009 +0200
+++ b/src/HOL/Nominal/nominal.ML	Tue Jun 23 16:27:12 2009 +0200
@@ -246,7 +246,7 @@
       Datatype.add_datatype config new_type_names' dts'' thy;
 
     val {descr, induction, ...} =
-      Datatype.the_datatype thy1 (hd full_new_type_names');
+      Datatype.the_info 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;