equal
deleted
inserted
replaced
91 val common_name = compatN ^ mk_common_name b_names; |
91 val common_name = compatN ^ mk_common_name b_names; |
92 val nn_fp = length fpTs; |
92 val nn_fp = length fpTs; |
93 val nn = length Ts; |
93 val nn = length Ts; |
94 val get_indices = K []; |
94 val get_indices = K []; |
95 val fp_sugars0 = if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts; |
95 val fp_sugars0 = if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts; |
96 val callssss = pad_and_indexify_calls fp_sugars0 nn []; |
96 val callssss = map (fn fp_sugar0 => indexify_callsss fp_sugar0 []) fp_sugars0; |
97 val has_nested = nn > nn_fp; |
97 val has_nested = nn > nn_fp; |
98 |
98 |
99 val ((fp_sugars, (lfp_sugar_thms, _)), lthy) = |
99 val ((fp_sugars, (lfp_sugar_thms, _)), lthy) = |
100 mutualize_fp_sugars has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy; |
100 mutualize_fp_sugars has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy; |
101 |
101 |