--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Apr 07 17:56:26 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Apr 07 17:56:26 2016 +0200
@@ -512,7 +512,7 @@
val fp_res =
({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
dtors = dtors, ctors = ctors,
- xtor_un_folds_legacy = xtor_co_recs (*wrong*), xtor_co_recs = xtor_co_recs,
+ xtor_un_folds = xtor_co_recs (*wrong*), xtor_co_recs = xtor_co_recs,
xtor_co_induct = xtor_co_induct_thm,
dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
@@ -522,13 +522,13 @@
xtor_map_unique = TrueI (*wrong*),
xtor_setss = of_fp_res #xtor_setss (*too general types and terms*),
xtor_rels = of_fp_res #xtor_rels (*too general types and terms*),
- xtor_un_fold_thms_legacy = xtor_co_rec_thms (*wrong*),
+ xtor_un_fold_thms = xtor_co_rec_thms (*wrong*),
xtor_co_rec_thms = xtor_co_rec_thms (*too general types and terms*),
- xtor_un_fold_unique_legacy = TrueI (*too general types and terms*),
+ xtor_un_fold_unique = TrueI (*too general types and terms*),
xtor_co_rec_unique = TrueI (*wrong*),
- xtor_un_fold_o_maps_legacy = fp_rec_o_maps (*wrong*),
+ xtor_un_fold_o_maps = fp_rec_o_maps (*wrong*),
xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
- xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [],
+ xtor_un_fold_transfers = [], xtor_co_rec_transfers = [],
xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
--- 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};
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Apr 07 17:56:26 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Apr 07 17:56:26 2016 +0200
@@ -2616,16 +2616,16 @@
val fp_res =
{Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
- ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = export corecs,
+ ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, xtor_co_recs = export corecs,
xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms,
xtor_map_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss',
- xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms_legacy = dtor_unfold_thms,
- xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_unique_legacy = dtor_unfold_unique_thm,
+ xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms = dtor_unfold_thms,
+ xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_unique = dtor_unfold_unique_thm,
xtor_co_rec_unique = dtor_corec_unique_thm,
- xtor_un_fold_o_maps_legacy = dtor_unfold_o_Jmap_thms,
+ xtor_un_fold_o_maps = dtor_unfold_o_Jmap_thms,
xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms,
- xtor_un_fold_transfers_legacy = dtor_unfold_transfer_thms,
+ xtor_un_fold_transfers = dtor_unfold_transfer_thms,
xtor_co_rec_transfers = dtor_corec_transfer_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
dtor_set_inducts = dtor_Jset_induct_thms};
in
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Apr 07 17:56:26 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Thu Apr 07 17:56:26 2016 +0200
@@ -2135,7 +2135,7 @@
val dead_pre_map = mk_map1 lthy Y Z preT dead_pre_bnf;
val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf;
val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT
- (the_single (#xtor_un_folds_legacy fp_res));
+ (the_single (#xtor_un_folds fp_res));
val Sig = mk_ctr As (the_single (#ctrs sig_ctr_sugar));
val unsig = mk_disc_or_sel As (the_single (the_single (#selss sig_ctr_sugar)));
val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf;
@@ -2159,9 +2159,9 @@
val [ctor_dtor] = #ctor_dtors fp_res;
val [dtor_ctor] = #dtor_ctors fp_res;
val [dtor_inject] = #dtor_injects fp_res;
- val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res;
- val dtor_unfold_unique = #xtor_un_fold_unique_legacy fp_res;
- val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res;
+ val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res;
+ val dtor_unfold_unique = #xtor_un_fold_unique fp_res;
+ val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res;
val [dtor_rel_thm] = #xtor_rels fp_res;
val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
val [sig_map_thm] = #map_thms sig_fp_bnf_sugar;
@@ -2369,7 +2369,7 @@
val dead_pre_rel = mk_rel1 lthy Y Z preT dead_pre_bnf;
val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf;
val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT
- (the_single (#xtor_un_folds_legacy fp_res));
+ (the_single (#xtor_un_folds fp_res));
val dead_k_map = mk_map1 lthy Y Z k_T dead_k_bnf;
val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar));
val unsig = mk_disc_or_sel res_As (the_single (the_single (#selss sig_ctr_sugar)));
@@ -2409,9 +2409,9 @@
val fp_map_id = map_id_of_bnf fp_bnf;
val [ctor_dtor] = #ctor_dtors fp_res;
val [dtor_inject] = #dtor_injects fp_res;
- val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res;
- val dtor_unfold_unique = #xtor_un_fold_unique_legacy fp_res;
- val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res;
+ val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res;
+ val dtor_unfold_unique = #xtor_un_fold_unique fp_res;
+ val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res;
val fp_k_T_rel_eqs =
map rel_eq_of_bnf (map_filter (bnf_of lthy) (fold add_type_namesT [fpT, k_T] []));
val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
@@ -2710,7 +2710,7 @@
val dead_pre_rel = mk_rel1 lthy Y Z preT dead_pre_bnf;
val fp_rel = mk_relN lthy live_EsFs fpT fp_bnf;
val dtor_unfold = mk_co_rec (Proof_Context.theory_of lthy) Greatest_FP [Z] fpT
- (the_single (#xtor_un_folds_legacy fp_res));
+ (the_single (#xtor_un_folds fp_res));
val Sig = mk_ctr res_As (the_single (#ctrs sig_ctr_sugar));
val unsig = mk_disc_or_sel res_As (the_single (the_single (#selss sig_ctr_sugar)));
val sig_rel = mk_relN lthy live_AsBs sig_T sig_bnf;
@@ -2761,9 +2761,9 @@
val fp_rel_eq = rel_eq_of_bnf fp_bnf;
val [ctor_dtor] = #ctor_dtors fp_res;
val [dtor_inject] = #dtor_injects fp_res;
- val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res;
- val dtor_unfold_unique = #xtor_un_fold_unique_legacy fp_res;
- val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res;
+ val [dtor_unfold_thm] = #xtor_un_fold_thms fp_res;
+ val dtor_unfold_unique = #xtor_un_fold_unique fp_res;
+ val [dtor_unfold_transfer] = #xtor_un_fold_transfers fp_res;
val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
val [sig_map_thm] = #map_thms sig_fp_bnf_sugar;
val old1_sig_map_comp = map_comp_of_bnf old1_sig_bnf;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 07 17:56:26 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 07 17:56:26 2016 +0200
@@ -1879,17 +1879,17 @@
val fp_res =
{Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
- ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = export recs,
+ ctors = ctors, dtors = dtors, xtor_un_folds = folds, xtor_co_recs = export recs,
xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms,
xtor_map_unique = ctor_Imap_unique_thm, xtor_setss = ctor_Iset_thmss',
- xtor_rels = ctor_Irel_thms, xtor_un_fold_thms_legacy = ctor_fold_thms,
- xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_unique_legacy = ctor_fold_unique_thm,
+ xtor_rels = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms,
+ xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_unique = ctor_fold_unique_thm,
xtor_co_rec_unique = ctor_rec_unique_thm,
- xtor_un_fold_o_maps_legacy = ctor_fold_o_Imap_thms,
+ xtor_un_fold_o_maps = ctor_fold_o_Imap_thms,
xtor_co_rec_o_maps = ctor_rec_o_Imap_thms,
- xtor_un_fold_transfers_legacy = ctor_fold_transfer_thms,
+ xtor_un_fold_transfers = ctor_fold_transfer_thms,
xtor_co_rec_transfers = ctor_rec_transfer_thms, xtor_rel_co_induct = Irel_induct_thm,
dtor_set_inducts = []};
in
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Apr 07 17:56:26 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Apr 07 17:56:26 2016 +0200
@@ -36,15 +36,15 @@
val co_rec_unique_thm = map_id0_of_bnf fp_bnf RS @{thm ctor_rec_unique};
in
{Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT],
- ctors = xtors, dtors = xtors, xtor_un_folds_legacy = co_recs,
+ ctors = xtors, dtors = xtors, xtor_un_folds = co_recs,
xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor},
ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject},
dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map],
xtor_map_unique = @{thm xtor_map_unique}, xtor_setss = [xtor_sets], xtor_rels = [xtor_rel],
- xtor_un_fold_thms_legacy = co_rec_thms, xtor_co_rec_thms = co_rec_thms,
- xtor_un_fold_unique_legacy = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm,
- xtor_un_fold_o_maps_legacy = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map],
- xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [],
+ xtor_un_fold_thms = co_rec_thms, xtor_co_rec_thms = co_rec_thms,
+ xtor_un_fold_unique = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm,
+ xtor_un_fold_o_maps = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map],
+ xtor_un_fold_transfers = [], xtor_co_rec_transfers = [],
xtor_rel_co_induct = xtor_rel_induct, dtor_set_inducts = []}
end;