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 23:53:10 2012 +0200
     1.3 @@ -498,17 +498,17 @@
     1.4      val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
     1.5      val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
     1.6  
     1.7 -    fun mk_map live' Ts Us t =
     1.8 -      let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN live' (fastype_of t) |>> List.last in
     1.9 +    fun mk_map live Ts Us t =
    1.10 +      let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
    1.11          Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    1.12        end;
    1.13  
    1.14      fun build_map build_arg (T as Type (s, Ts)) (U as Type (_, Us)) =
    1.15        let
    1.16          val bnf = the (bnf_of lthy s);
    1.17 -        val live' = live_of_bnf bnf + 1;
    1.18 -        val mapx = mk_map live' Ts Us (map_of_bnf bnf);
    1.19 -        val TUs = map dest_funT (fst (split_last (fst (strip_typeN live' (fastype_of mapx)))));
    1.20 +        val live = live_of_bnf bnf;
    1.21 +        val mapx = mk_map live Ts Us (map_of_bnf bnf);
    1.22 +        val TUs = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
    1.23          val args = map build_arg TUs;
    1.24        in Term.list_comb (mapx, args) end;
    1.25