--- a/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 24 12:21:19 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 24 12:21:19 2015 +0200
@@ -817,7 +817,7 @@
let
val live = length set_rhss;
- val def_qualify = Binding.concealed o Binding.qualify false (Binding.name_of bnf_b);
+ val def_qualify = Binding.qualify false (Binding.name_of bnf_b);
fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
@@ -837,7 +837,7 @@
let val b = b () in
apfst (apsnd snd)
((if internal then Local_Theory.define_internal else Local_Theory.define)
- ((b, NoSyn), ((Thm.def_binding b, []), rhs)) lthy)
+ ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []), rhs)) lthy)
end
end;