--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Apr 07 17:56:26 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Apr 07 17:56:26 2016 +0200
@@ -17,7 +17,7 @@
absT_infos: BNF_Comp.absT_info list,
ctors: term list,
dtors: term list,
- xtor_un_folds_legacy: term list,
+ xtor_un_folds: term list,
xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
@@ -28,13 +28,13 @@
xtor_map_unique: thm,
xtor_setss: thm list list,
xtor_rels: thm list,
- xtor_un_fold_thms_legacy: thm list,
+ xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list,
- xtor_un_fold_unique_legacy: thm,
+ xtor_un_fold_unique: thm,
xtor_co_rec_unique: thm,
- xtor_un_fold_o_maps_legacy: thm list,
+ xtor_un_fold_o_maps: thm list,
xtor_co_rec_o_maps: thm list,
- xtor_un_fold_transfers_legacy: thm list,
+ xtor_un_fold_transfers: thm list,
xtor_co_rec_transfers: thm list,
xtor_rel_co_induct: thm,
dtor_set_inducts: thm list}
@@ -228,7 +228,7 @@
absT_infos: BNF_Comp.absT_info list,
ctors: term list,
dtors: term list,
- xtor_un_folds_legacy: term list,
+ xtor_un_folds: term list,
xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
@@ -239,22 +239,22 @@
xtor_map_unique: thm,
xtor_setss: thm list list,
xtor_rels: thm list,
- xtor_un_fold_thms_legacy: thm list,
+ xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list,
- xtor_un_fold_unique_legacy: thm,
+ xtor_un_fold_unique: thm,
xtor_co_rec_unique: thm,
- xtor_un_fold_o_maps_legacy: thm list,
+ xtor_un_fold_o_maps: thm list,
xtor_co_rec_o_maps: thm list,
- xtor_un_fold_transfers_legacy: thm list,
+ xtor_un_fold_transfers: 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,
+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_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,
+ xtor_map_unique, xtor_setss, xtor_rels, xtor_un_fold_thms, xtor_co_rec_thms,
+ xtor_un_fold_unique, xtor_co_rec_unique, 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} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
@@ -262,7 +262,7 @@
absT_infos = map (morph_absT_info phi) absT_infos,
ctors = map (Morphism.term phi) ctors,
dtors = map (Morphism.term phi) dtors,
- xtor_un_folds_legacy = map (Morphism.term phi) xtor_un_folds_legacy,
+ xtor_un_folds = map (Morphism.term phi) xtor_un_folds,
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,
@@ -273,13 +273,13 @@
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_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
- xtor_un_fold_unique_legacy = Morphism.thm phi xtor_un_fold_unique_legacy,
+ xtor_un_fold_unique = Morphism.thm phi xtor_un_fold_unique,
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_un_fold_o_maps = map (Morphism.thm phi) xtor_un_fold_o_maps,
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_un_fold_transfers = map (Morphism.thm phi) xtor_un_fold_transfers,
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};