src/HOL/Tools/BNF/bnf_comp.ML

     val set_defs = set_defs_of_bnf bnf'';
     val rel_def = rel_def_of_bnf bnf'';
 
     val bnf_b = qualify b;
     val def_qualify =
-      Thm.def_binding o Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
+      Thm.def_binding o Binding.concealed o Binding.qualify false (Binding.name_of bnf_b);
     fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
     val map_b = def_qualify (mk_prefix_binding mapN);
     val rel_b = def_qualify (mk_prefix_binding relN);
     val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)]
       else map (def_qualify o mk_prefix_binding o mk_setN) (1 upto live);