src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

 fun define_co_rec_as fp Cs fpT b rhs lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
     val maybe_conceal_def_binding = Thm.def_binding
-      #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
+      #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
 
     val ((cst, (_, def)), (lthy', lthy)) = lthy0
       |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
       ||> `Local_Theory.restore;
 

         val ctr_rhss =
           map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs))
             ks xss;
 
         val maybe_conceal_def_binding = Thm.def_binding
-          #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.conceal;
+          #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.concealed;
 
         val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
           |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
               Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
             ctr_bindings ctr_mixfixes ctr_rhss