# HG changeset patch
# User blanchet
# Date 1347131066 -7200
# Node ID 0c9546fc789fb9e725b72a5673b5b51c2fc3922a
# Parent  e6fc5a6b152d02adb83a95849d87a6ea8767cf21
fixed handling of map of "fun"

diff -r e6fc5a6b152d -r 0c9546fc789f src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -30,6 +30,9 @@
 fun split_list8 xs =
   (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs);
 
+fun strip_map_type (Type (@{type_name fun}, [T as Type _, T'])) = strip_map_type T' |>> cons T
+  | strip_map_type T = ([], T);
+
 fun typ_subst inst (T as Type (s, Ts)) =
     (case AList.lookup (op =) inst T of
       NONE => Type (s, map (typ_subst inst) Ts)
@@ -421,7 +424,7 @@
       end;
 
     fun mk_map Ts Us t =
-      let val (Type (_, Ts0), Type (_, Us0)) = strip_type (fastype_of t) |>> List.last in
+      let val (Type (_, Ts0), Type (_, Us0)) = strip_map_type (fastype_of t) |>> List.last in
         Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
       end;
 
@@ -449,7 +452,8 @@
                       let
                         val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
                         val mapx = mk_map Ts Us map0;
-                        val TUs = map dest_funT (fst (split_last (binder_types (fastype_of mapx))));
+                        val TUs =
+                          map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
                         val args = map build TUs;
                       in Term.list_comb (mapx, args) end
                     | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j))
diff -r e6fc5a6b152d -r 0c9546fc789f src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -51,14 +51,15 @@
   Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
 
 val iter_like_thms =
-  @{thms sum_map.simps sum.simps(5,6) convol_def case_unit map_pair_def split_conv id_def};
+  @{thms case_unit comp_def convol_def id_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
 
 fun mk_iter_like_tac iter_like_defs fld_iter_likes ctr_def pre_map_def ctxt =
   Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
-  Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
+  Local_Defs.unfold_tac ctxt iter_like_thms THEN
+  rtac refl 1;
 
 val coiter_like_ss = ss_only @{thms if_True if_False};
-val coiter_like_thms = @{thms sum_map.simps map_pair_def id_def prod.cases};
+val coiter_like_thms = @{thms id_def map_pair_def sum_map.simps prod.cases};
 
 fun mk_coiter_like_tac coiter_like_defs fld_unf_coiter_like pre_map_def ctr_def ctxt =
   Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN