--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Sep 12 17:13:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Sep 12 17:18:20 2013 +0200
@@ -542,9 +542,12 @@
let
val thy = Proof_Context.theory_of lthy0;
+ val maybe_conceal_def_binding = Thm.def_binding
+ #> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
+
val ((csts, defs), (lthy', lthy)) = lthy0
|> apfst split_list o fold_map (fn (b, spec) =>
- Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
+ Specification.definition (SOME (b, NONE, NoSyn), ((maybe_conceal_def_binding b, []), spec))
#>> apsnd snd) binding_specs
||> `Local_Theory.restore;
@@ -1250,9 +1253,12 @@
map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $
mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs;
+ val maybe_conceal_def_binding = Thm.def_binding
+ #> Config.get no_defs_lthy bnf_note_all = false ? Binding.conceal;
+
val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
|> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
- Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
+ Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
ctr_bindings ctr_mixfixes ctr_rhss
||> `Local_Theory.restore;