--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:41:37 2014 +0200
@@ -1934,7 +1934,7 @@
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
- ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rel_thms,
+ ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
xtor_co_rec_transfers, ...},
lthy)) =
@@ -2360,7 +2360,7 @@
|> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
|> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
- pre_rel_defs ~~ xtor_maps ~~ xtor_setss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~
+ pre_rel_defs ~~ xtor_maps ~~ xtor_setss ~~ xtor_rels ~~ ns ~~ kss ~~ mss ~~
abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_default_eqss)
|> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:41:37 2014 +0200
@@ -473,7 +473,7 @@
dtor_injects = of_fp_res #dtor_injects (*too general types*),
xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
xtor_setss = of_fp_res #xtor_setss (*too general types and terms*),
- xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
+ xtor_rels = of_fp_res #xtor_rels (*too general types and terms*),
xtor_co_rec_thms = xtor_co_rec_thms,
xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
xtor_rel_co_induct = xtor_rel_co_induct,
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:41:37 2014 +0200
@@ -23,7 +23,7 @@
dtor_injects: thm list,
xtor_maps: thm list,
xtor_setss: thm list list,
- xtor_rel_thms: thm list,
+ xtor_rels: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_maps: thm list,
xtor_rel_co_induct: thm,
@@ -215,7 +215,7 @@
dtor_injects: thm list,
xtor_maps: thm list,
xtor_setss: thm list list,
- xtor_rel_thms: thm list,
+ xtor_rels: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_maps: thm list,
xtor_rel_co_induct: thm,
@@ -224,7 +224,7 @@
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss,
- xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
+ xtor_rels, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
dtor_set_inducts, xtor_co_rec_transfers} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
@@ -238,7 +238,7 @@
dtor_injects = map (Morphism.thm phi) dtor_injects,
xtor_maps = map (Morphism.thm phi) xtor_maps,
xtor_setss = map (map (Morphism.thm phi)) xtor_setss,
- xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
+ xtor_rels = map (Morphism.thm phi) xtor_rels,
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:41:37 2014 +0200
@@ -2540,7 +2540,7 @@
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_setss = dtor_Jset_thmss',
- xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
+ xtor_rels = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
dtor_set_inducts = dtor_Jset_induct_thms,
xtor_co_rec_transfers = dtor_corec_transfer_thms};
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:41:37 2014 +0200
@@ -1827,7 +1827,7 @@
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_setss = ctor_Iset_thmss',
- xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
+ xtor_rels = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_rel_co_induct = Irel_induct_thm,
dtor_set_inducts = [], xtor_co_rec_transfers = ctor_rec_transfer_thms};
in
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:40:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:41:37 2014 +0200
@@ -43,7 +43,7 @@
dtor_injects = @{thms xtor_inject},
xtor_maps = [xtor_map],
xtor_setss = [xtor_sets],
- xtor_rel_thms = [xtor_rel],
+ xtor_rels = [xtor_rel],
xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
xtor_co_rec_o_maps = [ctor_rec_o_map],
xtor_rel_co_induct = xtor_rel_induct,