src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55414 eab03e9cee8a
parent 55394 d5ebe055b599
child 55478 3a6efda01da4
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4      val dest_co_algT = co_swap o dest_funT;
     1.5      val co_alg_argT = fp_case fp range_type domain_type;
     1.6      val co_alg_funT = fp_case fp domain_type range_type;
     1.7 -    val mk_co_product = curry (fp_case fp mk_convol mk_sum_case);
     1.8 +    val mk_co_product = curry (fp_case fp mk_convol mk_case_sum);
     1.9      val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map;
    1.10      val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    1.11      val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
    1.12 @@ -336,7 +336,7 @@
    1.13            o_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
    1.14          val rec_thms = fold_thms @ fp_case fp
    1.15            @{thms fst_convol map_pair_o_convol convol_o}
    1.16 -          @{thms sum_case_o_inj(1) sum_case_o_sum_map o_sum_case};
    1.17 +          @{thms case_sum_o_inj(1) case_sum_o_sum_map o_case_sum};
    1.18          val map_thms = no_refl (maps (fn bnf =>
    1.19            [map_comp0_of_bnf bnf RS sym, map_id0_of_bnf bnf]) fp_nesty_bnfs);
    1.20