# HG changeset patch
# User traytel
# Date 1443090079 -7200
# Node ID 69a97fc33f7a3b7a6fc56372285f490bedc7edb7
# Parent  464c5da3f508b7949a65ea7703a6a2ff303558c1
conceal only the definitional theorems of map, set, rel (and not the actual constants)

diff -r 464c5da3f508 -r 69a97fc33f7a src/HOL/Tools/BNF/bnf_def.ML
--- 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;