# HG changeset patch # User blanchet # Date 1392742347 -3600 # Node ID ab0a547b5aeed4f768b299fd08ebbeaf8158bfb3 # Parent fd9ea8ae28f6c1c72740a66b08a670bb17363c56 made SML/NJ happier diff -r fd9ea8ae28f6 -r ab0a547b5aee src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Feb 18 14:51:26 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Feb 18 17:52:27 2014 +0100 @@ -45,7 +45,7 @@ Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g end; -fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy = +fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs lthy = let fun steal_fp_res get = map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;