1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 18:55:10 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 19:05:53 2012 +0200
     1.3 @@ -43,6 +43,8 @@
     1.4  
     1.5  val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs))
     1.6  
     1.7 +fun mk_id T = Const (@{const_name id}, T --> T);
     1.8 +
     1.9  fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
    1.10  fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
    1.11  fun mk_uncurried2_fun f xss =
    1.12 @@ -452,6 +454,14 @@
    1.13          Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    1.14        end;
    1.15  
    1.16 +    fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
    1.17 +      let
    1.18 +        val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
    1.19 +        val mapx = mk_map Ts Us map0;
    1.20 +        val TUs = map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
    1.21 +        val args = map build_arg TUs;
    1.22 +      in Term.list_comb (mapx, args) end;
    1.23 +
    1.24      fun pour_more_sugar_on_lfps ((ctrss, iters, recs, vs, xsss, ctr_defss, iter_defs, rec_defs),
    1.25          lthy) =
    1.26        let
    1.27 @@ -465,23 +475,13 @@
    1.28                fold_rev (fold_rev Logic.all) (xs :: fss)
    1.29                  (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
    1.30  
    1.31 -            fun build_call fiter_likes maybe_tick =
    1.32 -              let
    1.33 -                fun build (T, U) =
    1.34 -                  if T = U then
    1.35 -                    Const (@{const_name id}, T --> T)
    1.36 -                  else
    1.37 -                    (case (find_index (curry (op =) T) fpTs, (T, U)) of
    1.38 -                      (~1, (Type (s, Ts), Type (_, Us))) =>
    1.39 -                      let
    1.40 -                        val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
    1.41 -                        val mapx = mk_map Ts Us map0;
    1.42 -                        val TUs =
    1.43 -                          map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
    1.44 -                        val args = map build TUs;
    1.45 -                      in Term.list_comb (mapx, args) end
    1.46 -                    | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j))
    1.47 -              in build end;
    1.48 +            fun build_call fiter_likes maybe_tick (T, U) =
    1.49 +              if T = U then
    1.50 +                mk_id T
    1.51 +              else
    1.52 +                (case find_index (curry (op =) T) fpTs of
    1.53 +                  ~1 => build_map (build_call fiter_likes maybe_tick) T U
    1.54 +                | j => maybe_tick (nth vs j) (nth fiter_likes j));
    1.55  
    1.56              fun mk_U maybe_prodT =
    1.57                typ_subst (map2 (fn fpT => fn C => (fpT, maybe_prodT fpT C)) fpTs Cs);
    1.58 @@ -540,23 +540,13 @@
    1.59                  (Logic.list_implies (seq_conds mk_goal_cond n k cps,
    1.60                     mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, cfs'))));
    1.61  
    1.62 -            fun build_call fiter_likes maybe_tack =
    1.63 -              let
    1.64 -                fun build (T, U) =
    1.65 -                  if T = U then
    1.66 -                    Const (@{const_name id}, T --> T)
    1.67 -                  else
    1.68 -                    (case (find_index (curry (op =) U) fpTs, (T, U)) of
    1.69 -                      (~1, (Type (s, Ts), Type (_, Us))) =>
    1.70 -                      let
    1.71 -                        val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
    1.72 -                        val mapx = mk_map Ts Us map0;
    1.73 -                        val TUs =
    1.74 -                          map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
    1.75 -                        val args = map build TUs;
    1.76 -                      in Term.list_comb (mapx, args) end
    1.77 -                    | (j, _) => maybe_tack (nth cs j, nth vs j) (nth fiter_likes j))
    1.78 -              in build end;
    1.79 +            fun build_call fiter_likes maybe_tack (T, U) =
    1.80 +              if T = U then
    1.81 +                mk_id T
    1.82 +              else
    1.83 +                (case find_index (curry (op =) U) fpTs of
    1.84 +                  ~1 => build_map (build_call fiter_likes maybe_tack) T U
    1.85 +                | j => maybe_tack (nth cs j, nth vs j) (nth fiter_likes j));
    1.86  
    1.87              fun mk_U maybe_sumT =
    1.88                typ_subst (map2 (fn C => fn fpT => (maybe_sumT fpT C, fpT)) Cs fpTs);