--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jan 07 15:50:09 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jan 07 15:53:39 2016 +0100
@@ -1283,12 +1283,10 @@
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';
@@ -2201,14 +2199,12 @@
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';