properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
authorblanchet
Thu Nov 07 00:37:18 2013 +0100 (2013-11-07)
changeset 5428622616f65d4ea
parent 54285 578371ba74cc
child 54287 7f096d8eb3d0
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
src/HOL/BNF/Tools/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 23:05:44 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Thu Nov 07 00:37:18 2013 +0100
     1.3 @@ -10,9 +10,8 @@
     1.4    val unfold_let: term -> term
     1.5    val dest_map: Proof.context -> string -> term -> term * term list
     1.6  
     1.7 -  val mutualize_fp_sugars: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list ->
     1.8 -    (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list ->
     1.9 -    local_theory ->
    1.10 +  val mutualize_fp_sugars: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
    1.11 +    term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
    1.12      (BNF_FP_Def_Sugar.fp_sugar list
    1.13       * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
    1.14      * local_theory
    1.15 @@ -109,157 +108,150 @@
    1.16    Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
    1.17  
    1.18  (* TODO: test with sort constraints on As *)
    1.19 -(* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
    1.20 -   as deads? *)
    1.21 -fun mutualize_fp_sugars has_nested fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
    1.22 -  if has_nested then
    1.23 -    let
    1.24 -      val thy = Proof_Context.theory_of no_defs_lthy0;
    1.25 +fun mutualize_fp_sugars fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
    1.26 +  let
    1.27 +    val thy = Proof_Context.theory_of no_defs_lthy0;
    1.28  
    1.29 -      val qsotm = quote o Syntax.string_of_term no_defs_lthy0;
    1.30 +    val qsotm = quote o Syntax.string_of_term no_defs_lthy0;
    1.31  
    1.32 -      fun incompatible_calls t1 t2 =
    1.33 -        error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ qsotm t1 ^ " vs. " ^
    1.34 -          qsotm t2);
    1.35 +    fun incompatible_calls t1 t2 =
    1.36 +      error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ qsotm t1 ^ " vs. " ^ qsotm t2);
    1.37  
    1.38 -      val b_names = map Binding.name_of bs;
    1.39 -      val fp_b_names = map base_name_of_typ fpTs;
    1.40 +    val b_names = map Binding.name_of bs;
    1.41 +    val fp_b_names = map base_name_of_typ fpTs;
    1.42  
    1.43 -      val nn = length fpTs;
    1.44 +    val nn = length fpTs;
    1.45  
    1.46 -      fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
    1.47 -        let
    1.48 -          val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
    1.49 -          val phi = Morphism.term_morphism (Term.subst_TVars rho);
    1.50 -        in
    1.51 -          morph_ctr_sugar phi (nth ctr_sugars index)
    1.52 -        end;
    1.53 +    fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
    1.54 +      let
    1.55 +        val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
    1.56 +        val phi = Morphism.term_morphism (Term.subst_TVars rho);
    1.57 +      in
    1.58 +        morph_ctr_sugar phi (nth ctr_sugars index)
    1.59 +      end;
    1.60  
    1.61 -      val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
    1.62 -      val mapss = map (of_fp_sugar #mapss) fp_sugars0;
    1.63 -      val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
    1.64 +    val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
    1.65 +    val mapss = map (of_fp_sugar #mapss) fp_sugars0;
    1.66 +    val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
    1.67  
    1.68 -      val ctrss = map #ctrs ctr_sugars0;
    1.69 -      val ctr_Tss = map (map fastype_of) ctrss;
    1.70 +    val ctrss = map #ctrs ctr_sugars0;
    1.71 +    val ctr_Tss = map (map fastype_of) ctrss;
    1.72  
    1.73 -      val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
    1.74 -      val As = map TFree As';
    1.75 +    val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
    1.76 +    val As = map TFree As';
    1.77  
    1.78 -      val ((Cs, Xs), no_defs_lthy) =
    1.79 -        no_defs_lthy0
    1.80 -        |> fold Variable.declare_typ As
    1.81 -        |> mk_TFrees nn
    1.82 -        ||>> variant_tfrees fp_b_names;
    1.83 +    val ((Cs, Xs), no_defs_lthy) =
    1.84 +      no_defs_lthy0
    1.85 +      |> fold Variable.declare_typ As
    1.86 +      |> mk_TFrees nn
    1.87 +      ||>> variant_tfrees fp_b_names;
    1.88  
    1.89 -      fun check_call_dead live_call call =
    1.90 -        if null (get_indices call) then () else incompatible_calls live_call call;
    1.91 +    fun check_call_dead live_call call =
    1.92 +      if null (get_indices call) then () else incompatible_calls live_call call;
    1.93  
    1.94 -      fun freeze_fpTs_simple (T as Type (s, Ts)) =
    1.95 -          (case find_index (curry (op =) T) fpTs of
    1.96 -            ~1 => Type (s, map freeze_fpTs_simple Ts)
    1.97 -          | kk => nth Xs kk)
    1.98 -        | freeze_fpTs_simple T = T;
    1.99 +    fun freeze_fpTs_simple (T as Type (s, Ts)) =
   1.100 +        (case find_index (curry (op =) T) fpTs of
   1.101 +          ~1 => Type (s, map freeze_fpTs_simple Ts)
   1.102 +        | kk => nth Xs kk)
   1.103 +      | freeze_fpTs_simple T = T;
   1.104  
   1.105 -      fun freeze_fpTs_map (callss, (live_call :: _, dead_calls)) s Ts =
   1.106 -        (List.app (check_call_dead live_call) dead_calls;
   1.107 -         Type (s, map2 freeze_fpTs (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
   1.108 -           (transpose callss)) Ts))
   1.109 -      and freeze_fpTs calls (T as Type (s, Ts)) =
   1.110 -          (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
   1.111 -            ([], _) =>
   1.112 -            (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
   1.113 -              ([], _) => freeze_fpTs_simple T
   1.114 -            | callsp => freeze_fpTs_map callsp s Ts)
   1.115 +    fun freeze_fpTs_map (callss, (live_call :: _, dead_calls)) s Ts =
   1.116 +      (List.app (check_call_dead live_call) dead_calls;
   1.117 +       Type (s, map2 freeze_fpTs (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
   1.118 +         (transpose callss)) Ts))
   1.119 +    and freeze_fpTs calls (T as Type (s, Ts)) =
   1.120 +        (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
   1.121 +          ([], _) =>
   1.122 +          (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
   1.123 +            ([], _) => freeze_fpTs_simple T
   1.124            | callsp => freeze_fpTs_map callsp s Ts)
   1.125 -        | freeze_fpTs _ T = T;
   1.126 +        | callsp => freeze_fpTs_map callsp s Ts)
   1.127 +      | freeze_fpTs _ T = T;
   1.128  
   1.129 -      val ctr_Tsss = map (map binder_types) ctr_Tss;
   1.130 -      val ctrXs_Tsss = map2 (map2 (map2 freeze_fpTs)) callssss ctr_Tsss;
   1.131 -      val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
   1.132 -      val Ts = map (body_type o hd) ctr_Tss;
   1.133 +    val ctr_Tsss = map (map binder_types) ctr_Tss;
   1.134 +    val ctrXs_Tsss = map2 (map2 (map2 freeze_fpTs)) callssss ctr_Tsss;
   1.135 +    val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
   1.136 +    val Ts = map (body_type o hd) ctr_Tss;
   1.137  
   1.138 -      val ns = map length ctr_Tsss;
   1.139 -      val kss = map (fn n => 1 upto n) ns;
   1.140 -      val mss = map (map length) ctr_Tsss;
   1.141 +    val ns = map length ctr_Tsss;
   1.142 +    val kss = map (fn n => 1 upto n) ns;
   1.143 +    val mss = map (map length) ctr_Tsss;
   1.144  
   1.145 -      val fp_eqs = map dest_TFree Xs ~~ ctrXs_sum_prod_Ts;
   1.146 -      val key = key_of_fp_eqs fp fpTs fp_eqs;
   1.147 -    in
   1.148 -      (case n2m_sugar_of no_defs_lthy key of
   1.149 -        SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
   1.150 -      | NONE =>
   1.151 -        let
   1.152 -          val base_fp_names = Name.variant_list [] fp_b_names;
   1.153 -          val fp_bs = map2 (fn b_name => fn base_fp_name =>
   1.154 -              Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
   1.155 -            b_names base_fp_names;
   1.156 +    val fp_eqs = map dest_TFree Xs ~~ ctrXs_sum_prod_Ts;
   1.157 +    val key = key_of_fp_eqs fp fpTs fp_eqs;
   1.158 +  in
   1.159 +    (case n2m_sugar_of no_defs_lthy key of
   1.160 +      SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
   1.161 +    | NONE =>
   1.162 +      let
   1.163 +        val base_fp_names = Name.variant_list [] fp_b_names;
   1.164 +        val fp_bs = map2 (fn b_name => fn base_fp_name =>
   1.165 +            Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
   1.166 +          b_names base_fp_names;
   1.167  
   1.168 -          val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
   1.169 -                 dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
   1.170 -            fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' fp_eqs no_defs_lthy;
   1.171 +        val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_injects,
   1.172 +               dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
   1.173 +          fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' fp_eqs no_defs_lthy;
   1.174  
   1.175 -          val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
   1.176 -          val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
   1.177 +        val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
   1.178 +        val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
   1.179  
   1.180 -          val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
   1.181 -            mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
   1.182 +        val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
   1.183 +          mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
   1.184  
   1.185 -          fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
   1.186 +        fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
   1.187  
   1.188 -          val ((co_iterss, co_iter_defss), lthy) =
   1.189 -            fold_map2 (fn b =>
   1.190 -              (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
   1.191 -               else define_coiters [unfoldN, corecN] (the coiters_args_types))
   1.192 -                (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
   1.193 -            |>> split_list;
   1.194 +        val ((co_iterss, co_iter_defss), lthy) =
   1.195 +          fold_map2 (fn b =>
   1.196 +            (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
   1.197 +             else define_coiters [unfoldN, corecN] (the coiters_args_types))
   1.198 +              (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
   1.199 +          |>> split_list;
   1.200  
   1.201 -          val rho = tvar_subst thy Ts fpTs;
   1.202 -          val ctr_sugar_phi =
   1.203 -            Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
   1.204 -              (Morphism.term_morphism (Term.subst_TVars rho));
   1.205 -          val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
   1.206 +        val rho = tvar_subst thy Ts fpTs;
   1.207 +        val ctr_sugar_phi = Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
   1.208 +            (Morphism.term_morphism (Term.subst_TVars rho));
   1.209 +        val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
   1.210  
   1.211 -          val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
   1.212 +        val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
   1.213  
   1.214 -          val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
   1.215 -                sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
   1.216 -            if fp = Least_FP then
   1.217 -              derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
   1.218 -                xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
   1.219 -                co_iterss co_iter_defss lthy
   1.220 -              |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
   1.221 -                ([induct], fold_thmss, rec_thmss, [], [], [], []))
   1.222 -              ||> (fn info => (SOME info, NONE))
   1.223 -            else
   1.224 -              derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types)
   1.225 -                xtor_co_induct dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs
   1.226 -                ctrXs_Tsss kss mss ns ctr_defss ctr_sugars co_iterss co_iter_defss
   1.227 -                (Proof_Context.export lthy no_defs_lthy) lthy
   1.228 -              |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
   1.229 -                      (disc_unfold_thmss, disc_corec_thmss, _), _,
   1.230 -                      (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
   1.231 -                (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
   1.232 -                 disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
   1.233 -              ||> (fn info => (NONE, SOME info));
   1.234 +        val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
   1.235 +              sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
   1.236 +          if fp = Least_FP then
   1.237 +            derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
   1.238 +              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
   1.239 +              co_iterss co_iter_defss lthy
   1.240 +            |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
   1.241 +              ([induct], fold_thmss, rec_thmss, [], [], [], []))
   1.242 +            ||> (fn info => (SOME info, NONE))
   1.243 +          else
   1.244 +            derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
   1.245 +              dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
   1.246 +              ns ctr_defss ctr_sugars co_iterss co_iter_defss
   1.247 +              (Proof_Context.export lthy no_defs_lthy) lthy
   1.248 +            |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
   1.249 +                    (disc_unfold_thmss, disc_corec_thmss, _), _,
   1.250 +                    (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
   1.251 +              (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
   1.252 +               disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
   1.253 +            ||> (fn info => (NONE, SOME info));
   1.254  
   1.255 -          val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
   1.256 +        val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
   1.257  
   1.258 -          fun mk_target_fp_sugar (kk, T) =
   1.259 -            {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
   1.260 -             nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
   1.261 -             ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
   1.262 -             co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
   1.263 -             disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
   1.264 -             sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
   1.265 -            |> morph_fp_sugar phi;
   1.266 +        fun mk_target_fp_sugar (kk, T) =
   1.267 +          {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
   1.268 +           nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
   1.269 +           ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
   1.270 +           co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
   1.271 +           disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
   1.272 +           sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
   1.273 +          |> morph_fp_sugar phi;
   1.274  
   1.275 -          val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms);
   1.276 -        in
   1.277 -          (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
   1.278 -        end)
   1.279 -    end
   1.280 -  else
   1.281 -    ((fp_sugars0, (NONE, NONE)), no_defs_lthy0);
   1.282 +        val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms);
   1.283 +      in
   1.284 +        (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
   1.285 +      end)
   1.286 +  end;
   1.287  
   1.288  fun indexify_callsss fp_sugar callsss =
   1.289    let
   1.290 @@ -295,7 +287,7 @@
   1.291  
   1.292      val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
   1.293  
   1.294 -    val perm_actual_Ts as Type (_, tyargs0) :: _ =
   1.295 +    val perm_actual_Ts =
   1.296        sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
   1.297  
   1.298      fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s)));
   1.299 @@ -318,8 +310,8 @@
   1.300          fold (fold_subtype_pairs maybe_insert) (ctr_Ts ~~ gen_ctr_Ts) []
   1.301        end;
   1.302  
   1.303 -    fun check_enrich_with_mutuals _ _ seen gen_seen [] = (seen, gen_seen)
   1.304 -      | check_enrich_with_mutuals lthy rho seen gen_seen ((T as Type (_, tyargs)) :: Ts) =
   1.305 +    fun gather_types _ _ num_groups seen gen_seen [] = (num_groups, seen, gen_seen)
   1.306 +      | gather_types lthy rho num_groups seen gen_seen ((T as Type (_, tyargs)) :: Ts) =
   1.307          let
   1.308            val {fp_res = {Ts = mutual_Ts0, ...}, ...} = the_fp_sugar_of T;
   1.309            val mutual_Ts = map (retypargs tyargs) mutual_Ts0;
   1.310 @@ -354,11 +346,12 @@
   1.311            val gen_mutual_Ts = map (retypargs gen_tyargs) mutual_Ts0;
   1.312            val Ts' = filter_out (member (op =) mutual_Ts) Ts;
   1.313          in
   1.314 -          check_enrich_with_mutuals lthy' rho' (seen @ mutual_Ts) (gen_seen' @ gen_mutual_Ts) Ts'
   1.315 +          gather_types lthy' rho' (num_groups + 1) (seen @ mutual_Ts) (gen_seen' @ gen_mutual_Ts)
   1.316 +            Ts'
   1.317          end
   1.318 -      | check_enrich_with_mutuals _ _ _ _ (T :: _) = not_co_datatype T;
   1.319 +      | gather_types _ _ _ _ _ (T :: _) = not_co_datatype T;
   1.320  
   1.321 -    val (perm_Ts, perm_gen_Ts) = check_enrich_with_mutuals lthy [] [] [] perm_actual_Ts;
   1.322 +    val (num_groups, perm_Ts, perm_gen_Ts) = gather_types lthy [] 0 [] [] perm_actual_Ts;
   1.323      val perm_frozen_gen_Ts = map Logic.unvarifyT_global perm_gen_Ts;
   1.324  
   1.325      val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
   1.326 @@ -380,14 +373,16 @@
   1.327      val perm_callssss0 = permute callssss0;
   1.328      val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
   1.329  
   1.330 -    val has_nested = exists (fn Type (_, tyargs) => tyargs <> tyargs0) Ts;
   1.331      val perm_callssss = map2 indexify_callsss perm_fp_sugars0 perm_callssss0;
   1.332  
   1.333      val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
   1.334  
   1.335      val ((perm_fp_sugars, fp_sugar_thms), lthy) =
   1.336 -      mutualize_fp_sugars has_nested fp perm_bs perm_frozen_gen_Ts get_perm_indices perm_callssss
   1.337 -        perm_fp_sugars0 lthy;
   1.338 +      if num_groups > 1 then
   1.339 +        mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts get_perm_indices perm_callssss
   1.340 +          perm_fp_sugars0 lthy
   1.341 +      else
   1.342 +        ((perm_fp_sugars0, (NONE, NONE)), lthy);
   1.343  
   1.344      val fp_sugars = unpermute perm_fp_sugars;
   1.345    in
     2.1 --- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Wed Nov 06 23:05:44 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Thu Nov 07 00:37:18 2013 +0100
     2.3 @@ -94,10 +94,12 @@
     2.4      val get_indices = K [];
     2.5      val fp_sugars0 = if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts;
     2.6      val callssss = map (fn fp_sugar0 => indexify_callsss fp_sugar0 []) fp_sugars0;
     2.7 -    val has_nested = nn > nn_fp;
     2.8  
     2.9      val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
    2.10 -      mutualize_fp_sugars has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy;
    2.11 +      if nn > nn_fp then
    2.12 +        mutualize_fp_sugars Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy
    2.13 +      else
    2.14 +        ((fp_sugars0, (NONE, NONE)), lthy);
    2.15  
    2.16      val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
    2.17        fp_sugars;