# HG changeset patch # User desharna # Date 1412595656 -7200 # Node ID b6492a7abb59a538d5658f064b4daa5dac4be5dc # Parent 1dd83cbba63637a39bd9b3a23b5464e9a443b1d0 rename 'xtor_set_thmss' to 'xtor_setss' diff -r 1dd83cbba636 -r b6492a7abb59 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:40:31 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:40:56 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_set_thmss, xtor_rel_thms, + ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rel_thms, 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_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~ + pre_rel_defs ~~ xtor_maps ~~ xtor_setss ~~ xtor_rel_thms ~~ 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 diff -r 1dd83cbba636 -r b6492a7abb59 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:40:31 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:40:56 2014 +0200 @@ -472,7 +472,7 @@ ctor_injects = of_fp_res #ctor_injects (*too general types*), dtor_injects = of_fp_res #dtor_injects (*too general types*), xtor_maps = of_fp_res #xtor_maps (*too general types and terms*), - xtor_set_thmss = of_fp_res #xtor_set_thmss (*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_co_rec_thms = xtor_co_rec_thms, xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*), diff -r 1dd83cbba636 -r b6492a7abb59 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:40:31 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:40:56 2014 +0200 @@ -22,7 +22,7 @@ ctor_injects: thm list, dtor_injects: thm list, xtor_maps: thm list, - xtor_set_thmss: thm list list, + xtor_setss: thm list list, xtor_rel_thms: thm list, xtor_co_rec_thms: thm list, xtor_co_rec_o_maps: thm list, @@ -214,7 +214,7 @@ ctor_injects: thm list, dtor_injects: thm list, xtor_maps: thm list, - xtor_set_thmss: thm list list, + xtor_setss: thm list list, xtor_rel_thms: thm list, xtor_co_rec_thms: thm list, xtor_co_rec_o_maps: thm list, @@ -223,7 +223,7 @@ xtor_co_rec_transfers: 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_maps, xtor_set_thmss, + 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, dtor_set_inducts, xtor_co_rec_transfers} = {Ts = map (Morphism.typ phi) Ts, @@ -237,7 +237,7 @@ ctor_injects = map (Morphism.thm phi) ctor_injects, dtor_injects = map (Morphism.thm phi) dtor_injects, xtor_maps = map (Morphism.thm phi) xtor_maps, - xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, + xtor_setss = map (map (Morphism.thm phi)) xtor_setss, xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, 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, diff -r 1dd83cbba636 -r b6492a7abb59 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:40:31 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:40:56 2014 +0200 @@ -2539,7 +2539,7 @@ {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = 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_set_thmss = dtor_Jset_thmss', + xtor_maps = dtor_Jmap_thms, xtor_setss = dtor_Jset_thmss', xtor_rel_thms = 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, diff -r 1dd83cbba636 -r b6492a7abb59 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:40:31 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:40:56 2014 +0200 @@ -1826,7 +1826,7 @@ {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = 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_set_thmss = ctor_Iset_thmss', + xtor_maps = ctor_Imap_thms, xtor_setss = ctor_Iset_thmss', xtor_rel_thms = 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}; diff -r 1dd83cbba636 -r b6492a7abb59 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:40:31 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:40:56 2014 +0200 @@ -42,7 +42,7 @@ ctor_injects = @{thms xtor_inject}, dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], - xtor_set_thmss = [xtor_sets], + xtor_setss = [xtor_sets], xtor_rel_thms = [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],