made SML/NJ happier
authorblanchet
Tue Feb 18 17:52:27 2014 +0100 (2014-02-18)
changeset 55566ab0a547b5aee
parent 55541 fd9ea8ae28f6
child 55567 260e18aa306f
made SML/NJ happier
src/HOL/Tools/BNF/bnf_fp_n2m.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Feb 18 14:51:26 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Feb 18 17:52:27 2014 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4      Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
     1.5    end;
     1.6  
     1.7 -fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
     1.8 +fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs lthy =
     1.9    let
    1.10      fun steal_fp_res get =
    1.11        map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;