# HG changeset patch
# User blanchet
# Date 1382103775 -7200
# Node ID a8cf84bfa9beab42d4de658f158297b78fad7191
# Parent  b964fad0cbbd55d104f43a40dec7c7b3df6b9e49
conceal even more ugly constructions

diff -r b964fad0cbbd -r a8cf84bfa9be src/HOL/BNF/Tools/bnf_def.ML
--- 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;