--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 16:35:53 2014 +0200
@@ -27,7 +27,8 @@
xtor_co_rec_thms: thm list,
xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm,
- dtor_set_induct_thms: thm list}
+ dtor_set_induct_thms: thm list,
+ ctor_rec_transfer_thms: thm list}
val morph_fp_result: morphism -> fp_result -> fp_result
@@ -218,11 +219,13 @@
xtor_co_rec_thms: thm list,
xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm,
- dtor_set_induct_thms: thm list};
+ dtor_set_induct_thms: thm list,
+ ctor_rec_transfer_thms: thm list};
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
- xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms} =
+ xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm,
+ dtor_set_induct_thms, ctor_rec_transfer_thms} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
@@ -239,7 +242,8 @@
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
- dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *)
+ dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
+ ctor_rec_transfer_thms = map (Morphism.thm phi) ctor_rec_transfer_thms};
fun time ctxt timer msg = (if Config.get ctxt bnf_timing
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^