src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55931 62156e694f3d
parent 55899 8c0a13e84963
child 55932 68c5104d2204
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 12:17:26 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 13:36:15 2014 +0100
     1.3 @@ -38,12 +38,12 @@
     1.4        fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
     1.5    end;
     1.6  
     1.7 -fun mk_sum_map f g =
     1.8 +fun mk_map_sum f g =
     1.9    let
    1.10      val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    1.11      val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    1.12    in
    1.13 -    Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
    1.14 +    Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
    1.15    end;
    1.16  
    1.17  fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
    1.18 @@ -61,7 +61,7 @@
    1.19      val co_alg_argT = fp_case fp range_type domain_type;
    1.20      val co_alg_funT = fp_case fp domain_type range_type;
    1.21      val mk_co_product = curry (fp_case fp mk_convol mk_case_sum);
    1.22 -    val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map;
    1.23 +    val mk_map_co_product = fp_case fp mk_prod_map mk_map_sum;
    1.24      val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
    1.25      val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
    1.26      val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
    1.27 @@ -404,11 +404,11 @@
    1.28          val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
    1.29  
    1.30          val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
    1.31 -          map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp sum_map.comp} @
    1.32 -          @{thms id_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
    1.33 +          map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp map_sum.comp} @
    1.34 +          @{thms id_apply comp_id id_comp map_pair.comp map_pair.id map_sum.comp map_sum.id};
    1.35          val rec_thms = fold_thms @ fp_case fp
    1.36            @{thms fst_convol map_pair_o_convol convol_o}
    1.37 -          @{thms case_sum_o_inj(1) case_sum_o_sum_map o_case_sum};
    1.38 +          @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
    1.39  
    1.40          val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
    1.41