src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55067 a452de24a877
parent 55061 a0adf838e2d1
child 55394 d5ebe055b599
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -332,8 +332,8 @@
     1.4          val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
     1.5          val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
     1.6          val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
     1.7 -        val fold_thms = fp_case fp @{thm o_assoc[symmetric]} @{thm o_assoc} ::
     1.8 -          @{thms id_apply o_apply o_id id_o map_pair.comp map_pair.id sum_map.comp sum_map.id};
     1.9 +        val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
    1.10 +          o_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
    1.11          val rec_thms = fold_thms @ fp_case fp
    1.12            @{thms fst_convol map_pair_o_convol convol_o}
    1.13            @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};