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.concealed;
-
     val ((cst, (_, def)), (lthy', lthy)) = lthy0
       |> Local_Theory.open_target |> snd
-      |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
+      |> Local_Theory.define
+          ((b, NoSyn), ((Thm.make_def_binding (Config.get lthy0 bnf_internals) b, []), rhs))
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy lthy';
 
     val cst' = mk_co_rec thy fp Cs fpT (Morphism.term phi cst);

 
         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.concealed;
-
         val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
           |> Local_Theory.open_target |> snd
           |> 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
+              Local_Theory.define
+                ((b, mx), ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs))
+                  #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss
           ||> `Local_Theory.close_target;
 
         val phi = Proof_Context.export_morphism lthy lthy';
 
         val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;