document that n2m does not depend on most things in fp_sugar in its type

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 21 21:18:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Mar 22 07:18:36 2016 +0100
@@ -779,8 +779,8 @@
     (case (absT, absU) of
       (Type (C, Ts), Type (C', Us)) =>
         if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT
-        else raise Term.TYPE ("mk_repT", [absT, repT, absT], [])
-    | _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], []));
+        else raise Term.TYPE ("mk_repT", [absT, repT, absU], [])
+    | _ => raise Term.TYPE ("mk_repT", [absT, repT, absU], []));
 
 fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf}, _)) =
     Const (@{const_name id_bnf}, absU --> absU)

--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 21 21:18:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 22 07:18:36 2016 +0100
@@ -8,7 +8,7 @@
 signature BNF_FP_N2M =
 sig
   val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
-    BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
+    (int * BNF_FP_Util.fp_result) list -> binding list -> (string * sort) list ->
     typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
     BNF_FP_Util.fp_result * local_theory
 end;
@@ -47,12 +47,10 @@
     Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
   end;
 
-fun construct_mutualized_fp fp mutual_cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss)
-    bnfs (absT_infos : absT_info list) lthy =
+fun construct_mutualized_fp fp mutual_cliques fpTs (fp_results : (int * fp_result) list) bs resBs
+    (resDs, Dss) bnfs (absT_infos : absT_info list) lthy =
   let
-    fun of_fp_res get =
-      map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
-
+    fun of_fp_res get = map (uncurry nth o swap o apsnd get) fp_results;
     fun mk_co_algT T U = case_fp fp (T --> U) (U --> T);
     fun co_swap pair = case_fp fp I swap pair;
     val mk_co_comp = HOLogic.mk_comp o co_swap;
@@ -68,13 +66,9 @@
     val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT;
     val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp};
 
-    val fp_absT_infos = map #absT_info fp_sugars;
+    val fp_absT_infos = of_fp_res #absT_infos;
     val fp_bnfs = of_fp_res #bnfs;
-    val pre_bnfs = map #pre_bnf fp_sugars;
-    val nesting_bnfss =
-      map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars;
-    val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss;
-    val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (flat fp_or_nesting_bnfss);
+    val pre_bnfs = of_fp_res #pre_bnfs;
 
     val fp_absTs = map #absT fp_absT_infos;
     val fp_repTs = map #repT fp_absT_infos;
@@ -130,6 +124,15 @@
     val fp_repAs = map2 mk_rep absATs fp_reps;
     val fp_repBs = map2 mk_rep absBTs fp_reps;
 
+    val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
+    val sorted_theta = sort (int_ord o apply2 (Term.size_of_typ o fst)) (fpTs ~~ Xs)
+    val sorted_fpTs = map fst sorted_theta;
+
+    val nesting_bnfs = nesting_bnfs lthy
+      [[map (typ_subst_nonatomic_sorted (rev sorted_theta) o range_type o fastype_of) fp_repAs]]
+      allAs;
+    val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (fp_bnfs @ nesting_bnfs);
+
     val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
       |> mk_Frees' "R" phiTs
       ||>> mk_Frees "S" pre_phiTs
@@ -138,9 +141,9 @@
 
     val rels =
       let
-        fun find_rel T As Bs = fp_or_nesting_bnfss
-          |> map (filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf))
-          |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
+        fun find_rel T As Bs = fp_or_nesting_bnfs
+          |> filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf)
+          |> find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T))
           |> Option.map (fn bnf =>
             let val live = live_of_bnf bnf;
             in (mk_rel live As Bs (rel_of_bnf bnf), live) end)
@@ -258,9 +261,7 @@
       |> mk_Frees' "s" rec_strTs;
 
     val co_recs = of_fp_res #xtor_co_recs;
-    val ns = map (length o #Ts o #fp_res) fp_sugars;
-
-    val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
+    val ns = map (length o #Ts o snd) fp_results;
 
     fun foldT_of_recT recT =
       let
@@ -288,8 +289,7 @@
         val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
 
         val fold_pre_deads_only_Ts =
-          map (typ_subst_nonatomic_sorted (map (rpair dummyT)
-            (As @ sort (int_ord o apply2 Term.size_of_typ) fpTs))) fold_preTs';
+          map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ sorted_fpTs))) fold_preTs';
 
         val (mutual_clique, TUs) =
           map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
@@ -481,7 +481,8 @@
     (* These results are half broken. This is deliberate. We care only about those fields that are
        used by "primrec", "primcorecursive", and "datatype_compat". *)
     val fp_res =
-      ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors,
+      ({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
+        dtors = dtors, ctors = ctors,
         xtor_un_folds = co_recs (*wrong*), xtor_co_recs = co_recs,
         xtor_co_induct = xtor_co_induct_thm,
         dtor_ctors = of_fp_res #dtor_ctors (*too general types*),

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 21 21:18:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Mar 22 07:18:36 2016 +0100
@@ -242,9 +242,11 @@
 
         val fp_absT_infos = map #absT_info fp_sugars0;
 
+        val fp_results = map (apsnd #fp_res o `(#fp_res_index)) fp_sugars0
+
         val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
                dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
-          fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_sugars0) fp_bs
+          fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_results) fp_bs
             unsorted_As' killed_As' fp_eqs no_defs_lthy;
 
         val fp_abs_inverses = map #abs_inverse fp_absT_infos;

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 21 21:18:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 22 07:18:36 2016 +0100
@@ -13,6 +13,8 @@
   type fp_result =
     {Ts: typ list,
      bnfs: BNF_Def.bnf list,
+     pre_bnfs: BNF_Def.bnf list,
+     absT_infos: BNF_Comp.absT_info list,
      ctors: term list,
      dtors: term list,
      xtor_un_folds: term list,
@@ -213,6 +215,8 @@
 type fp_result =
   {Ts: typ list,
    bnfs: bnf list,
+   pre_bnfs: BNF_Def.bnf list,
+   absT_infos: BNF_Comp.absT_info list,
    ctors: term list,
    dtors: term list,
    xtor_un_folds: term list,
@@ -237,13 +241,15 @@
    xtor_rel_co_induct: thm,
    dtor_set_inducts: thm list};
 
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
-    dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_map_uniques, xtor_setss,
-    xtor_rels, xtor_un_fold_thms, xtor_co_rec_thms, xtor_un_fold_uniques, xtor_co_rec_uniques,
-    xtor_un_fold_o_maps, xtor_co_rec_o_maps, xtor_un_fold_transfers, xtor_co_rec_transfers,
-    xtor_rel_co_induct, dtor_set_inducts} =
+fun morph_fp_result phi {Ts, bnfs, pre_bnfs, absT_infos, ctors, dtors, xtor_un_folds, xtor_co_recs,
+    xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_map_uniques,
+    xtor_setss, xtor_rels, xtor_un_fold_thms, xtor_co_rec_thms, xtor_un_fold_uniques,
+    xtor_co_rec_uniques, xtor_un_fold_o_maps, xtor_co_rec_o_maps, xtor_un_fold_transfers,
+    xtor_co_rec_transfers, xtor_rel_co_induct, dtor_set_inducts} =
   {Ts = map (Morphism.typ phi) Ts,
    bnfs = map (morph_bnf phi) bnfs,
+   pre_bnfs = map (morph_bnf phi) pre_bnfs,
+   absT_infos = map (morph_absT_info phi) absT_infos,
    ctors = map (Morphism.term phi) ctors,
    dtors = map (Morphism.term phi) dtors,
    xtor_un_folds = map (Morphism.term phi) xtor_un_folds,

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 21 21:18:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 22 07:18:36 2016 +0100
@@ -56,7 +56,8 @@
      ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
 
 (*all BNFs have the same lives*)
-fun construct_gfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs _ lthy =
+fun construct_gfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs absT_infos
+    lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
@@ -2691,10 +2692,10 @@
     val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
 
     val fp_res =
-      {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds,
-       xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
-       ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
-       dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms,
+      {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
+       ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, xtor_co_recs = corecs,
+       xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
+       ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms,
        xtor_map_uniques = dtor_Jmap_unique_thms, xtor_setss = dtor_Jset_thmss',
        xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms = dtor_unfold_thms,
        xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_uniques = dtor_unfold_unique_thms,

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 21 21:18:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 22 07:18:36 2016 +0100
@@ -27,7 +27,8 @@
 open BNF_LFP_Tactics
 
 (*all BNFs have the same lives*)
-fun construct_lfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs _ lthy =
+fun construct_lfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs absT_infos
+    lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
@@ -1951,8 +1952,9 @@
     val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes);
 
     val fp_res =
-      {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds,
-       xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
+      {Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos,
+       ctors = ctors, dtors = dtors, xtor_un_folds = folds, xtor_co_recs = recs,
+       xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
        ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
        dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms,
        xtor_map_uniques = ctor_Imap_unique_thms, xtor_setss = ctor_Iset_thmss',

--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Mar 21 21:18:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Mar 22 07:18:36 2016 +0100
@@ -34,7 +34,8 @@
     val co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))];
     val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}];
   in
-    {Ts = [fpT], bnfs = [fp_bnf], ctors = xtors, dtors = xtors, xtor_un_folds = co_recs,
+    {Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT],
+     ctors = xtors, dtors = xtors, xtor_un_folds = co_recs,
      xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor},
      ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject},
      dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], xtor_map_uniques = [],