rename 'xtor_map_thms' to 'xtor_maps'
authordesharna
Mon Oct 06 13:40:31 2014 +0200 (2014-10-06)
changeset 585831dd83cbba636
parent 58582 a408c72a849c
child 58584 b6492a7abb59
rename 'xtor_map_thms' to 'xtor_maps'
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:40:02 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:40:31 2014 +0200
     1.3 @@ -1934,7 +1934,7 @@
     1.4  
     1.5      val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
     1.6               dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
     1.7 -             ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
     1.8 +             ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_set_thmss, xtor_rel_thms,
     1.9               xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
    1.10               xtor_co_rec_transfers, ...},
    1.11             lthy)) =
    1.12 @@ -2360,7 +2360,7 @@
    1.13        |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
    1.14        |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
    1.15          xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
    1.16 -        pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~
    1.17 +        pre_rel_defs ~~ xtor_maps ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~
    1.18          abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
    1.19          ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_default_eqss)
    1.20        |> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:40:02 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:40:31 2014 +0200
     2.3 @@ -471,7 +471,7 @@
     2.4          ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
     2.5          ctor_injects = of_fp_res #ctor_injects (*too general types*),
     2.6          dtor_injects = of_fp_res #dtor_injects (*too general types*),
     2.7 -        xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
     2.8 +        xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
     2.9          xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
    2.10          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
    2.11          xtor_co_rec_thms = xtor_co_rec_thms,
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:40:02 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:40:31 2014 +0200
     3.3 @@ -21,7 +21,7 @@
     3.4       ctor_dtors: thm list,
     3.5       ctor_injects: thm list,
     3.6       dtor_injects: thm list,
     3.7 -     xtor_map_thms: thm list,
     3.8 +     xtor_maps: thm list,
     3.9       xtor_set_thmss: thm list list,
    3.10       xtor_rel_thms: thm list,
    3.11       xtor_co_rec_thms: thm list,
    3.12 @@ -213,7 +213,7 @@
    3.13     ctor_dtors: thm list,
    3.14     ctor_injects: thm list,
    3.15     dtor_injects: thm list,
    3.16 -   xtor_map_thms: thm list,
    3.17 +   xtor_maps: thm list,
    3.18     xtor_set_thmss: thm list list,
    3.19     xtor_rel_thms: thm list,
    3.20     xtor_co_rec_thms: thm list,
    3.21 @@ -223,7 +223,7 @@
    3.22     xtor_co_rec_transfers: thm list};
    3.23  
    3.24  fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
    3.25 -    dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
    3.26 +    dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_set_thmss,
    3.27      xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
    3.28      dtor_set_inducts, xtor_co_rec_transfers} =
    3.29    {Ts = map (Morphism.typ phi) Ts,
    3.30 @@ -236,7 +236,7 @@
    3.31     ctor_dtors = map (Morphism.thm phi) ctor_dtors,
    3.32     ctor_injects = map (Morphism.thm phi) ctor_injects,
    3.33     dtor_injects = map (Morphism.thm phi) dtor_injects,
    3.34 -   xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
    3.35 +   xtor_maps = map (Morphism.thm phi) xtor_maps,
    3.36     xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
    3.37     xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
    3.38     xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:40:02 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:40:31 2014 +0200
     4.3 @@ -2539,7 +2539,7 @@
     4.4        {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs,
     4.5         xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
     4.6         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
     4.7 -       xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
     4.8 +       xtor_maps = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
     4.9         xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
    4.10         xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
    4.11         dtor_set_inducts = dtor_Jset_induct_thms,
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:40:02 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:40:31 2014 +0200
     5.3 @@ -1826,7 +1826,7 @@
     5.4        {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs,
     5.5         xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
     5.6         ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
     5.7 -       xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
     5.8 +       xtor_maps = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
     5.9         xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
    5.10         xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_rel_co_induct = Irel_induct_thm,
    5.11         dtor_set_inducts = [], xtor_co_rec_transfers = ctor_rec_transfer_thms};
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:40:02 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:40:31 2014 +0200
     6.3 @@ -41,7 +41,7 @@
     6.4     ctor_dtors = @{thms xtor_xtor},
     6.5     ctor_injects = @{thms xtor_inject},
     6.6     dtor_injects = @{thms xtor_inject},
     6.7 -   xtor_map_thms = [xtor_map],
     6.8 +   xtor_maps = [xtor_map],
     6.9     xtor_set_thmss = [xtor_sets],
    6.10     xtor_rel_thms = [xtor_rel],
    6.11     xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],