src/HOL/BNF/Tools/bnf_def.ML
changeset 54156 a8cf84bfa9be
parent 54045 369a4a14583a
child 54158 0af35cebe8ca
--- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Oct 18 15:25:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Oct 18 15:42:55 2013 +0200
@@ -633,7 +633,7 @@
         | T => err T)
       else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
 
-    val def_qualify = Binding.qualify false (Binding.name_of bnf_b);
+    val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
 
     fun mk_suffix_binding suf = Binding.suffix_name ("_" ^ suf) bnf_b;