src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
changeset 57983 6edc3529bb4e
parent 57897 36778ca6847c
child 58112 8081087096ad
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -257,7 +257,7 @@
     1.4              fp_bs xtor_co_recs lthy
     1.5            |>> split_list;
     1.6  
     1.7 -        val ((common_co_inducts, co_inductss, co_rec_thmss, disc_corec_thmss, sel_corec_thmsss),
     1.8 +        val ((common_co_inducts, co_inductss, co_rec_thmss, corec_disc_thmss, corec_sel_thmsss),
     1.9               fp_sugar_thms) =
    1.10            if fp = Least_FP then
    1.11              derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
    1.12 @@ -272,30 +272,30 @@
    1.13                dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
    1.14                mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
    1.15                ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
    1.16 -            |> `(fn ((coinduct_thms_pairs, _), corec_thmss, disc_corec_thmss, _,
    1.17 -                     (sel_corec_thmsss, _)) =>
    1.18 +            |> `(fn ((coinduct_thms_pairs, _), corec_thmss, corec_disc_thmss, _,
    1.19 +                     (corec_sel_thmsss, _)) =>
    1.20                (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
    1.21 -               disc_corec_thmss, sel_corec_thmsss))
    1.22 +               corec_disc_thmss, corec_sel_thmsss))
    1.23              ||> (fn info => (NONE, SOME info));
    1.24  
    1.25          val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
    1.26  
    1.27          fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
    1.28 -            co_rec_def maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss
    1.29 +            co_rec_def maps co_inducts co_rec_thms corec_disc_thms corec_sel_thmss
    1.30              ({rel_injects, rel_distincts, ...} : fp_sugar) =
    1.31            {T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
    1.32             fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info,
    1.33             fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
    1.34             ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
    1.35             co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts,
    1.36 -           co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
    1.37 -           sel_co_recss = sel_corec_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
    1.38 +           co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = corec_disc_thms,
    1.39 +           sel_co_recss = corec_sel_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
    1.40            |> morph_fp_sugar phi;
    1.41  
    1.42          val target_fp_sugars =
    1.43            map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
    1.44 -            co_recs co_rec_defs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss
    1.45 -            sel_corec_thmsss fp_sugars0;
    1.46 +            co_recs co_rec_defs mapss (transpose co_inductss) co_rec_thmss corec_disc_thmss
    1.47 +            corec_sel_thmsss fp_sugars0;
    1.48  
    1.49          val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
    1.50        in