src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

 
 fun split_list10 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,
    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)) =
     (case AList.lookup (op =) inst T of
       NONE => Type (s, map (typ_subst inst) Ts)

     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
     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;
 
     fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _,
         iter_defs, rec_defs), lthy) =