src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML

      funs: term list,
      fun_defs: thm list,
      fpTs: typ list}
 
   val morph_fp_rec_sugar: morphism -> fp_rec_sugar -> fp_rec_sugar
+  val transfer_fp_rec_sugar: theory -> fp_rec_sugar -> fp_rec_sugar
 
   val flat_rec_arg_args: 'a list list -> 'a list
 
   val indexed: 'a list -> int -> int list * int
   val indexedd: 'a list list -> int -> int list list * int

 type fp_rec_sugar =
   {transfers: bool list,
    fun_names: string list,
    funs: term list,
    fun_defs: thm list,
-   fpTs: typ list}
+   fpTs: typ list};
 
 fun morph_fp_rec_sugar phi {transfers, fun_names, funs, fun_defs, fpTs} =
   {transfers = transfers,
    fun_names = fun_names,
    funs = map (Morphism.term phi) funs,
    fun_defs = map (Morphism.thm phi) fun_defs,
    fpTs = map (Morphism.typ phi) fpTs};
 
+val transfer_fp_rec_sugar = morph_fp_rec_sugar o Morphism.transfer_morphism;
+
 fun flat_rec_arg_args xss =
-  (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
-     order. The second line is for compatibility with the old datatype package. *)
+  (* FIXME (once the old datatype package is completely phased out): The first line below gives the
+     preferred order. The second line is for compatibility with the old datatype package. *)
   (* flat xss *)
   map hd xss @ maps tl xss;
 
 fun indexe _ h = (h, h + 1);
 fun indexed xs = fold_map indexe xs;