# HG changeset patch
# User blanchet
# Date 1347736226 -7200
# Node ID e1f325ab95030206e0af406528a8335fe6a0b1f0
# Parent  3a96797fd53ebccf8948a35eef077a817737c81f
tuned code to avoid special case for "fun"

diff -r 3a96797fd53e -r e1f325ab9503 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 21:10:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 21:10:26 2012 +0200
@@ -38,9 +38,6 @@
   (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
    map #9 xs, map #10 xs);
 
-fun strip_map_type @{type_name fun} (Type (_, [T, Type (_, [T', T''])])) = ([T, T'], T'')
-  | strip_map_type _ T = strip_type T;
-
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
 
 fun typ_subst inst (T as Type (s, Ts)) =
@@ -501,16 +498,17 @@
     val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
     val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
 
-    fun mk_map s Ts Us t =
-      let val (Type (_, Ts0), Type (_, Us0)) = strip_map_type s (fastype_of t) |>> List.last in
+    fun mk_map live' Ts Us t =
+      let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN live' (fastype_of t) |>> List.last in
         Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
       end;
 
     fun build_map build_arg (T as Type (s, Ts)) (U as Type (_, Us)) =
       let
-        val map0 = map_of_bnf (the (bnf_of lthy s));
-        val mapx = mk_map s Ts Us map0;
-        val TUs = map dest_funT (fst (split_last (fst (strip_map_type s (fastype_of mapx)))));
+        val bnf = the (bnf_of lthy s);
+        val live' = live_of_bnf bnf + 1;
+        val mapx = mk_map live' Ts Us (map_of_bnf bnf);
+        val TUs = map dest_funT (fst (split_last (fst (strip_typeN live' (fastype_of mapx)))));
         val args = map build_arg TUs;
       in Term.list_comb (mapx, args) end;
 
diff -r 3a96797fd53e -r e1f325ab9503 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 15 21:10:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 15 21:10:26 2012 +0200
@@ -92,6 +92,7 @@
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
+  val strip_typeN: int -> typ -> typ list * typ
   val retype_free: typ -> term -> term
 
   val mk_predT: typ -> typ;
@@ -240,6 +241,9 @@
 
 val mk_common_name = space_implode "_" o map Binding.name_of;
 
+fun strip_typeN 0 T = ([], T)
+  | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T;
+
 fun mk_predT T = T --> HOLogic.boolT;
 
 fun retype_free T (Free (s, _)) = Free (s, T);