1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -30,6 +30,9 @@
     1.4  fun split_list8 xs =
     1.5    (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs);
     1.6  
     1.7 +fun strip_map_type (Type (@{type_name fun}, [T as Type _, T'])) = strip_map_type T' |>> cons T
     1.8 +  | strip_map_type T = ([], T);
     1.9 +
    1.10  fun typ_subst inst (T as Type (s, Ts)) =
    1.11      (case AList.lookup (op =) inst T of
    1.12        NONE => Type (s, map (typ_subst inst) Ts)
    1.13 @@ -421,7 +424,7 @@
    1.14        end;
    1.15  
    1.16      fun mk_map Ts Us t =
    1.17 -      let val (Type (_, Ts0), Type (_, Us0)) = strip_type (fastype_of t) |>> List.last in
    1.18 +      let val (Type (_, Ts0), Type (_, Us0)) = strip_map_type (fastype_of t) |>> List.last in
    1.19          Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    1.20        end;
    1.21  
    1.22 @@ -449,7 +452,8 @@
    1.23                        let
    1.24                          val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
    1.25                          val mapx = mk_map Ts Us map0;
    1.26 -                        val TUs = map dest_funT (fst (split_last (binder_types (fastype_of mapx))));
    1.27 +                        val TUs =
    1.28 +                          map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
    1.29                          val args = map build TUs;
    1.30                        in Term.list_comb (mapx, args) end
    1.31                      | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j))

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     2.3 @@ -51,14 +51,15 @@
     2.4    Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
     2.5  
     2.6  val iter_like_thms =
     2.7 -  @{thms sum_map.simps sum.simps(5,6) convol_def case_unit map_pair_def split_conv id_def};
     2.8 +  @{thms case_unit comp_def convol_def id_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
     2.9  
    2.10  fun mk_iter_like_tac iter_like_defs fld_iter_likes ctr_def pre_map_def ctxt =
    2.11    Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
    2.12 -  Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
    2.13 +  Local_Defs.unfold_tac ctxt iter_like_thms THEN
    2.14 +  rtac refl 1;
    2.15  
    2.16  val coiter_like_ss = ss_only @{thms if_True if_False};
    2.17 -val coiter_like_thms = @{thms sum_map.simps map_pair_def id_def prod.cases};
    2.18 +val coiter_like_thms = @{thms id_def map_pair_def sum_map.simps prod.cases};
    2.19  
    2.20  fun mk_coiter_like_tac coiter_like_defs fld_unf_coiter_like pre_map_def ctr_def ctxt =
    2.21    Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN