1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 21:10:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 15 21:10:26 2012 +0200
     1.3 @@ -38,9 +38,6 @@
     1.4    (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.5     map #9 xs, map #10 xs);
     1.6  
     1.7 -fun strip_map_type @{type_name fun} (Type (_, [T, Type (_, [T', T''])])) = ([T, T'], T'')
     1.8 -  | strip_map_type _ T = strip_type T;
     1.9 -
    1.10  fun resort_tfree S (TFree (s, _)) = TFree (s, S);
    1.11  
    1.12  fun typ_subst inst (T as Type (s, Ts)) =
    1.13 @@ -501,16 +498,17 @@
    1.14      val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
    1.15      val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
    1.16  
    1.17 -    fun mk_map s Ts Us t =
    1.18 -      let val (Type (_, Ts0), Type (_, Us0)) = strip_map_type s (fastype_of t) |>> List.last in
    1.19 +    fun mk_map live' Ts Us t =
    1.20 +      let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN live' (fastype_of t) |>> List.last in
    1.21          Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    1.22        end;
    1.23  
    1.24      fun build_map build_arg (T as Type (s, Ts)) (U as Type (_, Us)) =
    1.25        let
    1.26 -        val map0 = map_of_bnf (the (bnf_of lthy s));
    1.27 -        val mapx = mk_map s Ts Us map0;
    1.28 -        val TUs = map dest_funT (fst (split_last (fst (strip_map_type s (fastype_of mapx)))));
    1.29 +        val bnf = the (bnf_of lthy s);
    1.30 +        val live' = live_of_bnf bnf + 1;
    1.31 +        val mapx = mk_map live' Ts Us (map_of_bnf bnf);
    1.32 +        val TUs = map dest_funT (fst (split_last (fst (strip_typeN live' (fastype_of mapx)))));
    1.33          val args = map build_arg TUs;
    1.34        in Term.list_comb (mapx, args) end;
    1.35