--- a/src/HOL/Nominal/nominal_datatype.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Sep 17 08:23:53 2014 +0200
@@ -200,9 +200,9 @@
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
- val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype_dead BNF_LFP_Compat.Unfold_Nesting dts'' thy;
+ val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Kill_Type_Args] dts'' thy;
- val {descr, induct, ...} = BNF_LFP_Compat.the_info thy1 BNF_LFP_Compat.Unfold_Nesting (hd full_new_type_names');
+ val {descr, induct, ...} = BNF_LFP_Compat.the_info thy1 [] (hd full_new_type_names');
fun nth_dtyp i = Old_Datatype_Aux.typ_of_dtyp descr (Old_Datatype_Aux.DtRec i);
val big_name = space_implode "_" new_type_names;