src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55566 ab0a547b5aee
parent 55539 0819931d652d
child 55575 a5e33e18fb5c
equal deleted inserted replaced
55541:fd9ea8ae28f6 55566:ab0a547b5aee
    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;