# HG changeset patch # User desharna # Date 1412595520 -7200 # Node ID 8ee2d984caa84af144ef8c47059a140557d7a2ee # Parent b7bc5ba2f3fb952c2fdb642162e295616bbcb302 rename 'dtor_set_induct_thms' to 'dtor_set_inducts' diff -r b7bc5ba2f3fb -r 8ee2d984caa8 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:38:13 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:38:40 2014 +0200 @@ -1935,7 +1935,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_map_thms, xtor_set_thmss, xtor_rel_thms, - xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_induct_thms, + xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts, xtor_co_rec_transfer_thms, ...}, lthy)) = fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) @@ -2308,7 +2308,7 @@ val (set_induct_thms, set_induct_attrss) = derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars) - (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_induct_thms + (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_inducts (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss) dtor_ctors abs_inverses |> split_list; diff -r b7bc5ba2f3fb -r 8ee2d984caa8 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:38:13 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:38:40 2014 +0200 @@ -477,7 +477,7 @@ 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, - dtor_set_induct_thms = [], + dtor_set_inducts = [], xtor_co_rec_transfer_thms = []} |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); in diff -r b7bc5ba2f3fb -r 8ee2d984caa8 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:38:13 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:38:40 2014 +0200 @@ -27,7 +27,7 @@ xtor_co_rec_thms: thm list, xtor_co_rec_o_maps: thm list, xtor_rel_co_induct: thm, - dtor_set_induct_thms: thm list, + dtor_set_inducts: thm list, xtor_co_rec_transfer_thms: thm list} val morph_fp_result: morphism -> fp_result -> fp_result @@ -219,13 +219,13 @@ xtor_co_rec_thms: thm list, xtor_co_rec_o_maps: thm list, xtor_rel_co_induct: thm, - dtor_set_induct_thms: thm list, + dtor_set_inducts: thm list, xtor_co_rec_transfer_thms: 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_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct, - dtor_set_induct_thms, xtor_co_rec_transfer_thms} = + dtor_set_inducts, xtor_co_rec_transfer_thms} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, ctors = map (Morphism.term phi) ctors, @@ -242,7 +242,7 @@ 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, - dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms, + dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts, xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms}; fun time ctxt timer msg = (if Config.get ctxt bnf_timing diff -r b7bc5ba2f3fb -r 8ee2d984caa8 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:38:13 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:38:40 2014 +0200 @@ -2542,7 +2542,7 @@ xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = 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_induct_thms = dtor_Jset_induct_thms, + dtor_set_inducts = dtor_Jset_induct_thms, xtor_co_rec_transfer_thms = dtor_corec_transfer_thms}; in timer; (fp_res, lthy') diff -r b7bc5ba2f3fb -r 8ee2d984caa8 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:38:13 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:38:40 2014 +0200 @@ -1829,7 +1829,7 @@ xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = 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_induct_thms = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms}; + dtor_set_inducts = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms}; in timer; (fp_res, lthy') end; diff -r b7bc5ba2f3fb -r 8ee2d984caa8 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:38:13 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:38:40 2014 +0200 @@ -47,7 +47,7 @@ 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, - dtor_set_induct_thms = [], + dtor_set_inducts = [], xtor_co_rec_transfer_thms = []}; fun fp_sugar_of_sum ctxt =