src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55932 68c5104d2204
parent 55931 62156e694f3d
child 55966 972f0aa7091b
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 13:36:15 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 13:36:48 2014 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4      val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
     1.5      val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
     1.6    in
     1.7 -    Const (@{const_name map_pair},
     1.8 +    Const (@{const_name map_prod},
     1.9        fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
    1.10    end;
    1.11  
    1.12 @@ -404,10 +404,10 @@
    1.13          val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
    1.14  
    1.15          val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
    1.16 -          map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp map_sum.comp} @
    1.17 -          @{thms id_apply comp_id id_comp map_pair.comp map_pair.id map_sum.comp map_sum.id};
    1.18 +          map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
    1.19 +          @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
    1.20          val rec_thms = fold_thms @ fp_case fp
    1.21 -          @{thms fst_convol map_pair_o_convol convol_o}
    1.22 +          @{thms fst_convol map_prod_o_convol convol_o}
    1.23            @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
    1.24  
    1.25          val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;