--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 08 14:03:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 08 14:03:01 2014 +0200
@@ -526,7 +526,7 @@
val thy = Proof_Context.theory_of lthy0;
val maybe_conceal_def_binding = Thm.def_binding
- #> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
+ #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
val ((cst, (_, def)), (lthy', lthy)) = lthy0
|> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
@@ -1394,7 +1394,7 @@
ks xss;
val maybe_conceal_def_binding = Thm.def_binding
- #> Config.get no_defs_lthy bnf_note_all = false ? Binding.conceal;
+ #> not (Config.get no_defs_lthy bnf_note_all) ? 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 =>