--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 30 22:34:59 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 31 00:11:54 2015 +0200
@@ -984,7 +984,7 @@
|> map2 currys arg_Tss
|> (fn ts => Syntax.check_terms ctxt ts
handle ERROR _ => nonprimitive_corec 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
|> rpair excludess'
end;