properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
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;