--- 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);