src/HOL/Nominal/nominal_datatype.ML

     val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
 
     val (full_new_type_names',thy1) =
       Datatype.add_datatype config new_type_names' dts'' thy;
 
-    val {descr, inducts = (_, induct), ...} =
+    val {descr, induct, ...} =
       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;