conceal only the definitional theorems of map, set, rel (and not the actual constants)

--- 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;