--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 28 12:05:47 2016 +0200
@@ -17,7 +17,7 @@
absT_infos: BNF_Comp.absT_info list,
ctors: term list,
dtors: term list,
- xtor_un_folds: term list,
+ xtor_un_folds_legacy: term list,
xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
@@ -28,13 +28,13 @@
xtor_map_uniques: thm list,
xtor_setss: thm list list,
xtor_rels: thm list,
- xtor_un_fold_thms: thm list,
+ xtor_un_fold_thms_legacy: thm list,
xtor_co_rec_thms: thm list,
- xtor_un_fold_uniques: thm list,
+ xtor_un_fold_uniques_legacy: thm list,
xtor_co_rec_uniques: thm list,
- xtor_un_fold_o_maps: thm list,
+ xtor_un_fold_o_maps_legacy: thm list,
xtor_co_rec_o_maps: thm list,
- xtor_un_fold_transfers: 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}
@@ -220,7 +220,7 @@
absT_infos: BNF_Comp.absT_info list,
ctors: term list,
dtors: term list,
- xtor_un_folds: term list,
+ xtor_un_folds_legacy: term list,
xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
@@ -231,29 +231,30 @@
xtor_map_uniques: thm list,
xtor_setss: thm list list,
xtor_rels: thm list,
- xtor_un_fold_thms: thm list,
+ xtor_un_fold_thms_legacy: thm list,
xtor_co_rec_thms: thm list,
- xtor_un_fold_uniques: thm list,
+ xtor_un_fold_uniques_legacy: thm list,
xtor_co_rec_uniques: thm list,
- xtor_un_fold_o_maps: thm list,
+ xtor_un_fold_o_maps_legacy: thm list,
xtor_co_rec_o_maps: thm list,
- xtor_un_fold_transfers: 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, 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, xtor_co_rec_thms, xtor_un_fold_uniques,
- xtor_co_rec_uniques, xtor_un_fold_o_maps, xtor_co_rec_o_maps, xtor_un_fold_transfers,
- xtor_co_rec_transfers, xtor_rel_co_induct, dtor_set_inducts} =
+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_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,
absT_infos = map (morph_absT_info phi) absT_infos,
ctors = map (Morphism.term phi) ctors,
dtors = map (Morphism.term phi) dtors,
- xtor_un_folds = map (Morphism.term phi) xtor_un_folds,
+ xtor_un_folds_legacy = map (Morphism.term phi) xtor_un_folds_legacy,
xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
xtor_co_induct = Morphism.thm phi xtor_co_induct,
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
@@ -264,13 +265,13 @@
xtor_map_uniques = map (Morphism.thm phi) xtor_map_uniques,
xtor_setss = map (map (Morphism.thm phi)) xtor_setss,
xtor_rels = map (Morphism.thm phi) xtor_rels,
- xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
+ 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 = map (Morphism.thm phi) xtor_un_fold_uniques,
+ 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_o_maps = map (Morphism.thm phi) xtor_un_fold_o_maps,
+ 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 = map (Morphism.thm phi) xtor_un_fold_transfers,
+ 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,
dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts};