# HG changeset patch # User blanchet # Date 1467733928 -7200 # Node ID 6840e808fe4403c2255a83668185e4b1c0938d01 # Parent c27edca2d8279050c8bf73e302253b556119521a tuning diff -r c27edca2d827 -r 6840e808fe44 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Jul 05 17:52:08 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Jul 05 17:52:08 2016 +0200 @@ -1256,7 +1256,7 @@ let val T = fastype_of1 (bound_Ts, hd args) in (case (Option.mapPartial (ctr_sugar_of lthy) (try (fst o dest_Type) T), T <> res_T) of (SOME {selss, T = Type (_, Ts), ...}, true) => - (case const_of (fold (curry op @) selss []) fun_t of + (case const_of (flat selss) fun_t of SOME sel => let val args' = args |> map (typ_before explore params);