--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Mar 30 22:34:59 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Mar 31 00:11:54 2015 +0200
@@ -457,7 +457,7 @@
(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.conceal (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;