src/HOL/Nominal/nominal_datatype.ML

         map (fn (cname, cargs, mx) => (Binding.suffix_name "_Rep" cname,
           map replace_types cargs, NoSyn)) constrs)) dts';
 
     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 {descr, induct, ...} = Old_Datatype_Data.the_info thy1 (hd full_new_type_names');
+    val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting dts'' thy;
+
+    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;