--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Nov 30 19:12:08 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Dec 01 13:07:40 2015 +0100
@@ -458,7 +458,8 @@
(recs, ctr_poss)
|-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
|> Syntax.check_terms ctxt
- |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
+ |> @{map 3} (fn b => fn mx => fn t =>
+ ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
bs mxs
end;