conceal consts via name space, not tags;

--- a/src/HOL/Tools/res_axioms.ML	Sun Oct 25 12:27:21 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sun Oct 25 13:18:35 2009 +0100
@@ -85,7 +85,7 @@
             val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
                     (*Forms a lambda-abstraction over the formal parameters*)
             val (c, thy') =
-              Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy
+              Sign.declare_const [] ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
             val cdef = cname ^ "_def"
             val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
             val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)

--- a/src/Pure/General/markup.ML	Sun Oct 25 12:27:21 2009 +0100
+++ b/src/Pure/General/markup.ML	Sun Oct 25 13:18:35 2009 +0100
@@ -17,7 +17,6 @@
   val theory_nameN: string
   val kindN: string
   val internalK: string
-  val property_internal: Properties.property
   val entityN: string val entity: string -> T
   val defN: string
   val refN: string
@@ -161,7 +160,6 @@
 val kindN = "kind";
 
 val internalK = "internal";
-val property_internal = (kindN, internalK);
 
 
 (* formal entities *)

--- a/src/Pure/Tools/find_consts.ML	Sun Oct 25 12:27:21 2009 +0100
+++ b/src/Pure/Tools/find_consts.ML	Sun Oct 25 13:18:35 2009 +0100
@@ -87,9 +87,8 @@
     val thy = ProofContext.theory_of ctxt;
     val low_ranking = 10000;
 
-    fun not_internal consts (nm, _) =
-      if member (op =) (Consts.the_tags consts nm) Markup.property_internal
-      then NONE else SOME low_ranking;
+    fun user_visible consts (nm, _) =
+      if Consts.is_concealed consts nm then NONE else SOME low_ranking;
 
     fun make_pattern crit =
       let
@@ -119,7 +118,7 @@
     val consts = Sign.consts_of thy;
     val (_, consts_tab) = #constants (Consts.dest consts);
     fun eval_entry c =
-      fold filter_const (not_internal consts :: criteria)
+      fold filter_const (user_visible consts :: criteria)
         (SOME (c, low_ranking));
 
     val matches =

--- a/src/Pure/consts.ML	Sun Oct 25 12:27:21 2009 +0100
+++ b/src/Pure/consts.ML	Sun Oct 25 13:18:35 2009 +0100
@@ -20,6 +20,7 @@
   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
   val space_of: T -> Name_Space.T
+  val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val extern_early: T -> string -> xstring
@@ -123,6 +124,8 @@
 
 fun space_of (Consts {decls = (space, _), ...}) = space;
 
+val is_concealed = Name_Space.is_concealed o space_of;
+
 val intern = Name_Space.intern o space_of;
 val extern = Name_Space.extern o space_of;
 

--- a/src/Pure/display.ML	Sun Oct 25 12:27:21 2009 +0100
+++ b/src/Pure/display.ML	Sun Oct 25 13:18:35 2009 +0100
@@ -188,8 +188,7 @@
     val tdecls = Name_Space.dest_table types;
     val arties = Name_Space.dest_table (Sign.type_space thy, arities);
 
-    fun prune_const c = not verbose andalso
-      member (op =) (Consts.the_tags consts c) Markup.property_internal;
+    fun prune_const c = not verbose andalso Consts.is_concealed consts c;
     val cnsts = Name_Space.extern_table (#1 constants,
       Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));