--- a/src/HOL/Nominal/nominal_datatype.ML Mon Sep 08 20:42:52 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Mon Sep 08 23:04:18 2014 +0200
@@ -200,9 +200,9 @@
val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
- val (full_new_type_names',thy1) = Old_Datatype.add_datatype config dts'' thy;
+ val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting dts'' thy;
- val {descr, induct, ...} = Old_Datatype_Data.the_info thy1 (hd full_new_type_names');
+ val {descr, induct, ...} = BNF_LFP_Compat.the_info thy1 BNF_LFP_Compat.Unfold_Nesting (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;