src/HOL/Tools/BNF/bnf_fp_util.ML

      dtor_ctors: thm list,
      ctor_dtors: thm list,
      ctor_injects: thm list,
      dtor_injects: thm list,
      xtor_maps: thm list,
-     xtor_map_uniques: thm list,
+     xtor_map_unique: thm,
      xtor_setss: thm list list,
      xtor_rels: thm list,
      xtor_un_fold_thms_legacy: thm list,
      xtor_co_rec_thms: thm list,
-     xtor_un_fold_uniques_legacy: thm list,
-     xtor_co_rec_uniques: thm list,
+     xtor_un_fold_unique_legacy: thm,
+     xtor_co_rec_unique: thm,
      xtor_un_fold_o_maps_legacy: thm list,
      xtor_co_rec_o_maps: thm list,
      xtor_un_fold_transfers_legacy: thm list,
      xtor_co_rec_transfers: thm list,
      xtor_rel_co_induct: thm,

    dtor_ctors: thm list,
    ctor_dtors: thm list,
    ctor_injects: thm list,
    dtor_injects: thm list,
    xtor_maps: thm list,
-   xtor_map_uniques: thm list,
+   xtor_map_unique: thm,
    xtor_setss: thm list list,
    xtor_rels: thm list,
    xtor_un_fold_thms_legacy: thm list,
    xtor_co_rec_thms: thm list,
-   xtor_un_fold_uniques_legacy: thm list,
-   xtor_co_rec_uniques: thm list,
+   xtor_un_fold_unique_legacy: thm,
+   xtor_co_rec_unique: thm,
    xtor_un_fold_o_maps_legacy: thm list,
    xtor_co_rec_o_maps: thm list,
    xtor_un_fold_transfers_legacy: thm list,
    xtor_co_rec_transfers: thm list,
    xtor_rel_co_induct: thm,
    dtor_set_inducts: thm list};
 
 fun morph_fp_result phi {Ts, bnfs, pre_bnfs, absT_infos, ctors, dtors, xtor_un_folds_legacy,
     xtor_co_recs, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps,
-    xtor_map_uniques, xtor_setss, xtor_rels, xtor_un_fold_thms_legacy, xtor_co_rec_thms,
-    xtor_un_fold_uniques_legacy, xtor_co_rec_uniques, xtor_un_fold_o_maps_legacy,
+    xtor_map_unique, xtor_setss, xtor_rels, xtor_un_fold_thms_legacy, xtor_co_rec_thms,
+    xtor_un_fold_unique_legacy, xtor_co_rec_unique, xtor_un_fold_o_maps_legacy,
     xtor_co_rec_o_maps, xtor_un_fold_transfers_legacy, xtor_co_rec_transfers, xtor_rel_co_induct,
     dtor_set_inducts} =
   {Ts = map (Morphism.typ phi) Ts,
    bnfs = map (morph_bnf phi) bnfs,
    pre_bnfs = map (morph_bnf phi) pre_bnfs,

    dtor_ctors = map (Morphism.thm phi) dtor_ctors,
    ctor_dtors = map (Morphism.thm phi) ctor_dtors,
    ctor_injects = map (Morphism.thm phi) ctor_injects,
    dtor_injects = map (Morphism.thm phi) dtor_injects,
    xtor_maps = map (Morphism.thm phi) xtor_maps,
-   xtor_map_uniques = map (Morphism.thm phi) xtor_map_uniques,
+   xtor_map_unique = Morphism.thm phi xtor_map_unique,
    xtor_setss = map (map (Morphism.thm phi)) xtor_setss,
    xtor_rels = map (Morphism.thm phi) xtor_rels,
    xtor_un_fold_thms_legacy = map (Morphism.thm phi) xtor_un_fold_thms_legacy,
    xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
-   xtor_un_fold_uniques_legacy = map (Morphism.thm phi) xtor_un_fold_uniques_legacy,
-   xtor_co_rec_uniques = map (Morphism.thm phi) xtor_co_rec_uniques,
+   xtor_un_fold_unique_legacy = Morphism.thm phi xtor_un_fold_unique_legacy,
+   xtor_co_rec_unique = Morphism.thm phi xtor_co_rec_unique,
    xtor_un_fold_o_maps_legacy = map (Morphism.thm phi) xtor_un_fold_o_maps_legacy,
    xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
    xtor_un_fold_transfers_legacy = map (Morphism.thm phi) xtor_un_fold_transfers_legacy,
    xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers,
    xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,