equal
deleted
inserted
replaced
43 val ((gAT, gBT), gT) = `dest_funT (fastype_of g); |
43 val ((gAT, gBT), gT) = `dest_funT (fastype_of g); |
44 in |
44 in |
45 Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g |
45 Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g |
46 end; |
46 end; |
47 |
47 |
48 fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy = |
48 fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs lthy = |
49 let |
49 let |
50 fun steal_fp_res get = |
50 fun steal_fp_res get = |
51 map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars; |
51 map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars; |
52 |
52 |
53 val n = length bnfs; |
53 val n = length bnfs; |