src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML

     val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}];
   in
     {Ts = [fpT], bnfs = [fp_bnf], ctors = xtors, dtors = xtors, xtor_un_folds = co_recs,
      xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor},
      ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject},
-     dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], xtor_setss = [xtor_sets],
-     xtor_rels = [xtor_rel], xtor_un_fold_thms = co_rec_thms, xtor_co_rec_thms = co_rec_thms,
-     xtor_co_rec_o_maps = [ctor_rec_o_map], xtor_rel_co_induct = xtor_rel_induct,
-     dtor_set_inducts = [], xtor_co_rec_transfers = []}
+     dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], xtor_map_uniques = [],
+     xtor_setss = [xtor_sets], xtor_rels = [xtor_rel], xtor_un_fold_thms = co_rec_thms,
+     xtor_co_rec_thms = co_rec_thms, xtor_un_fold_uniques = [], xtor_co_rec_uniques = [],
+     xtor_un_fold_o_maps = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map],
+     xtor_un_fold_transfers = [], xtor_co_rec_transfers = [], xtor_rel_co_induct = xtor_rel_induct,
+     dtor_set_inducts = []}
   end;
 
 fun fp_sugar_of_sum ctxt =
   let
     val fpT as Type (fpT_name, As) = @{typ "'a + 'b"};