merged

--- a/src/HOL/Tools/res_axioms.ML	Sun Oct 25 13:14:00 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sun Oct 25 13:20:31 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/binding.ML	Sun Oct 25 13:14:00 2009 +0100
+++ b/src/Pure/General/binding.ML	Sun Oct 25 13:20:31 2009 +0100
@@ -10,7 +10,7 @@
 signature BINDING =
 sig
   type binding
-  val dest: binding -> (string * bool) list * bstring
+  val dest: binding -> bool * (string * bool) list * bstring
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
   val name: bstring -> binding
@@ -27,6 +27,7 @@
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding
+  val conceal: binding -> binding
   val str_of: binding -> string
 end;
 
@@ -38,19 +39,21 @@
 (* datatype *)
 
 abstype binding = Binding of
- {prefix: (string * bool) list,     (*system prefix*)
+ {conceal: bool,                    (*internal -- for foundational purposes only*)
+  prefix: (string * bool) list,     (*system prefix*)
   qualifier: (string * bool) list,  (*user qualifier*)
   name: bstring,                    (*base name*)
   pos: Position.T}                  (*source position*)
 with
 
-fun make_binding (prefix, qualifier, name, pos) =
-  Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
+fun make_binding (conceal, prefix, qualifier, name, pos) =
+  Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
 
-fun map_binding f (Binding {prefix, qualifier, name, pos}) =
-  make_binding (f (prefix, qualifier, name, pos));
+fun map_binding f (Binding {conceal, prefix, qualifier, name, pos}) =
+  make_binding (f (conceal, prefix, qualifier, name, pos));
 
-fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
+fun dest (Binding {conceal, prefix, qualifier, name, ...}) =
+  (conceal, prefix @ qualifier, name);
 
 
 
@@ -58,7 +61,7 @@
 
 (* name and position *)
 
-fun make (name, pos) = make_binding ([], [], name, pos);
+fun make (name, pos) = make_binding (false, [], [], name, pos);
 fun name name = make (name, Position.none);
 
 fun pos_of (Binding {pos, ...}) = pos;
@@ -66,7 +69,10 @@
 
 fun eq_name (b, b') = name_of b = name_of b';
 
-fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos));
+fun map_name f =
+  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
+    (conceal, prefix, qualifier, f name, pos));
+
 val prefix_name = map_name o prefix;
 val suffix_name = map_name o suffix;
 
@@ -77,13 +83,14 @@
 (* user qualifier *)
 
 fun qualify _ "" = I
-  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
-      (prefix, (qual, mandatory) :: qualifier, name, pos));
+  | qualify mandatory qual =
+      map_binding (fn (conceal, prefix, qualifier, name, pos) =>
+        (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
 
 fun qualified_name "" = empty
   | qualified_name s =
       let val (qualifier, name) = split_last (Long_Name.explode s)
-      in make_binding ([], map (rpair false) qualifier, name, Position.none) end;
+      in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;
 
 fun qualified_name_of (b as Binding {qualifier, name, ...}) =
   if is_empty b then ""
@@ -94,13 +101,21 @@
 
 fun prefix_of (Binding {prefix, ...}) = prefix;
 
-fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
-  (f prefix, qualifier, name, pos));
+fun map_prefix f =
+  map_binding (fn (conceal, prefix, qualifier, name, pos) =>
+    (conceal, f prefix, qualifier, name, pos));
 
 fun prefix _ "" = I
   | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
 
 
+(* conceal *)
+
+val conceal =
+  map_binding (fn (_, prefix, qualifier, name, pos) =>
+    (true, prefix, qualifier, name, pos));
+
+
 (* str_of *)
 
 fun str_of binding =

--- a/src/Pure/General/markup.ML	Sun Oct 25 13:14:00 2009 +0100
+++ b/src/Pure/General/markup.ML	Sun Oct 25 13:20:31 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/General/name_space.ML	Sun Oct 25 13:14:00 2009 +0100
+++ b/src/Pure/General/name_space.ML	Sun Oct 25 13:20:31 2009 +0100
@@ -22,22 +22,24 @@
   type T
   val empty: string -> T
   val kind_of: T -> string
-  val the_entry: T -> string -> {is_system: bool, pos: Position.T, id: serial}
+  val the_entry: T -> string -> {concealed: bool, pos: Position.T, id: serial}
+  val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
-  val extern: T -> string -> xstring
   val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
     T -> string -> xstring
+  val extern: T -> string -> xstring
   val hide: bool -> string -> T -> T
   val merge: T * T -> T
   type naming
   val default_naming: naming
-  val declare: bool -> naming -> binding -> T -> string * T
-  val full_name: naming -> binding -> string
-  val external_names: naming -> string -> string list
   val add_path: string -> naming -> naming
   val root_path: naming -> naming
   val parent_path: naming -> naming
   val mandatory_path: string -> naming -> naming
+  val conceal: naming -> naming
+  val full_name: naming -> binding -> string
+  val external_names: naming -> string -> string list
+  val declare: bool -> naming -> binding -> T -> string * T
   type 'a table = T * 'a Symtab.table
   val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   val empty_table: string -> 'a table
@@ -64,7 +66,7 @@
 
 type entry =
  {externals: xstring list,
-  is_system: bool,
+  concealed: bool,
   pos: Position.T,
   id: serial};
 
@@ -104,7 +106,9 @@
 fun the_entry (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
-  | SOME {is_system, pos, id, ...} => {is_system = is_system, pos = pos, id = id});
+  | SOME {concealed, pos, id, ...} => {concealed = concealed, pos = pos, id = id});
+
+fun is_concealed space name = #concealed (the_entry space name);
 
 
 (* name accesses *)
@@ -209,36 +213,41 @@
 
 (* datatype naming *)
 
-datatype naming = Naming of (string * bool) list;
-fun map_naming f (Naming path) = Naming (f path);
+datatype naming = Naming of bool * (string * bool) list;
 
-val default_naming = Naming [];
+fun map_naming f (Naming (conceal, path)) = Naming (f (conceal, path));
+fun map_path f = map_naming (apsnd f);
+
+val default_naming = Naming (false, []);
 
-fun add_path elems = map_naming (fn path => path @ [(elems, false)]);
-val root_path = map_naming (fn _ => []);
-val parent_path = map_naming (perhaps (try (#1 o split_last)));
-fun mandatory_path elems = map_naming (fn path => path @ [(elems, true)]);
+fun add_path elems = map_path (fn path => path @ [(elems, false)]);
+val root_path = map_path (fn _ => []);
+val parent_path = map_path (perhaps (try (#1 o split_last)));
+fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
+
+val conceal = map_naming (fn (_, path) => (true, path));
 
 
 (* full name *)
 
 fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
 
-fun name_spec (Naming path) binding =
+fun name_spec (Naming (conceal1, path)) binding =
   let
-    val (prefix, name) = Binding.dest binding;
+    val (conceal2, prefix, name) = Binding.dest binding;
     val _ = Long_Name.is_qualified name andalso err_bad binding;
 
+    val concealed = conceal1 orelse conceal2;
     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
     val spec2 = if name = "" then [] else [(name, true)];
     val spec = spec1 @ spec2;
     val _ =
       exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
       andalso err_bad binding;
-  in if null spec2 then [] else spec end;
+  in (concealed, if null spec2 then [] else spec) end;
 
-fun full naming = name_spec naming #> map fst;
-fun full_name naming = full naming #> Long_Name.implode;
+fun full_name naming =
+  name_spec naming #> snd #> map fst #> Long_Name.implode;
 
 
 (* accesses *)
@@ -254,7 +263,7 @@
 
 fun accesses naming binding =
   let
-    val spec = name_spec naming binding;
+    val spec = #2 (name_spec naming binding);
     val sfxs = mandatory_suffixes spec;
     val pfxs = mandatory_prefixes spec;
   in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
@@ -275,13 +284,15 @@
 
 fun declare strict naming binding space =
   let
-    val names = full naming binding;
-    val name = Long_Name.implode names;
+    val (concealed, spec) = name_spec naming binding;
+    val (accs, accs') = accesses naming binding;
+
+    val name = Long_Name.implode (map fst spec);
     val _ = name = "" andalso err_bad binding;
-    val (accs, accs') = accesses naming binding;
+
     val entry =
      {externals = accs',
-      is_system = false,
+      concealed = concealed,
       pos = Position.default (Binding.pos_of binding),
       id = serial ()};
     val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);

--- a/src/Pure/Isar/local_theory.ML	Sun Oct 25 13:14:00 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sun Oct 25 13:20:31 2009 +0100
@@ -72,12 +72,14 @@
 
 datatype lthy = LThy of
  {group: string,
+  conceal: bool,
   theory_prefix: string,
   operations: operations,
   target: Proof.context};
 
-fun make_lthy (group, theory_prefix, operations, target) =
-  LThy {group = group, theory_prefix = theory_prefix, operations = operations, target = target};
+fun make_lthy (group, conceal, theory_prefix, operations, target) =
+  LThy {group = group, conceal = conceal, theory_prefix = theory_prefix,
+    operations = operations, target = target};
 
 
 (* context data *)
@@ -94,8 +96,8 @@
   | SOME (LThy data) => data);
 
 fun map_lthy f lthy =
-  let val {group, theory_prefix, operations, target} = get_lthy lthy
-  in Data.put (SOME (make_lthy (f (group, theory_prefix, operations, target)))) lthy end;
+  let val {group, conceal, theory_prefix, operations, target} = get_lthy lthy
+  in Data.put (SOME (make_lthy (f (group, conceal, theory_prefix, operations, target)))) lthy end;
 
 
 (* group *)
@@ -110,8 +112,8 @@
 fun group_position_of lthy =
   group_properties_of lthy @ Position.properties_of (Position.thread_data ());
 
-fun set_group group = map_lthy (fn (_, theory_prefix, operations, target) =>
-  (group, theory_prefix, operations, target));
+fun set_group group = map_lthy (fn (_, conceal, theory_prefix, operations, target) =>
+  (group, conceal, theory_prefix, operations, target));
 
 
 (* target *)
@@ -119,8 +121,8 @@
 val target_of = #target o get_lthy;
 val affirm = tap target_of;
 
-fun map_target f = map_lthy (fn (group, theory_prefix, operations, target) =>
-  (group, theory_prefix, operations, f target));
+fun map_target f = map_lthy (fn (group, conceal, theory_prefix, operations, target) =>
+  (group, conceal, theory_prefix, operations, f target));
 
 
 (* substructure mappings *)
@@ -138,15 +140,22 @@
 val checkpoint = raw_theory Theory.checkpoint;
 
 fun full_naming lthy =
-  Sign.naming_of (ProofContext.theory_of lthy)
-  |> Name_Space.mandatory_path (#theory_prefix (get_lthy lthy));
+  let val {conceal, theory_prefix, ...} = get_lthy lthy in
+    Sign.naming_of (ProofContext.theory_of lthy)
+    |> Name_Space.mandatory_path theory_prefix
+    |> conceal ? Name_Space.conceal
+  end;
 
 fun full_name naming = Name_Space.full_name (full_naming naming);
 
-fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
-  |> Sign.mandatory_path (#theory_prefix (get_lthy lthy))
-  |> f
-  ||> Sign.restore_naming thy);
+fun theory_result f lthy = lthy |> raw_theory_result (fn thy =>
+  let val {conceal, theory_prefix, ...} = get_lthy lthy in
+    thy
+    |> Sign.mandatory_path theory_prefix
+    |> conceal ? Sign.conceal
+    |> f
+    ||> Sign.restore_naming thy
+  end);
 
 fun theory f = #2 o theory_result (f #> pair ());
 
@@ -197,12 +206,12 @@
 (* init *)
 
 fun init theory_prefix operations target = target |> Data.map
-  (fn NONE => SOME (make_lthy ("", theory_prefix, operations, target))
+  (fn NONE => SOME (make_lthy ("", false, theory_prefix, operations, target))
     | SOME _ => error "Local theory already initialized")
   |> checkpoint;
 
 fun restore lthy =
-  let val {group = _, theory_prefix, operations, target} = get_lthy lthy
+  let val {theory_prefix, operations, target, ...} = get_lthy lthy
   in init theory_prefix operations target end;
 
 val reinit = checkpoint o operation #reinit;

--- a/src/Pure/Isar/proof_context.ML	Sun Oct 25 13:14:00 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Oct 25 13:20:31 2009 +0100
@@ -94,6 +94,7 @@
   val get_thm: Proof.context -> xstring -> thm
   val add_path: string -> Proof.context -> Proof.context
   val mandatory_path: string -> Proof.context -> Proof.context
+  val conceal: Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
@@ -926,6 +927,7 @@
 
 val add_path = map_naming o Name_Space.add_path;
 val mandatory_path = map_naming o Name_Space.mandatory_path;
+val conceal = map_naming Name_Space.conceal;
 val restore_naming = map_naming o K o naming_of;
 val reset_naming = map_naming (K local_naming);
 

--- a/src/Pure/Tools/find_consts.ML	Sun Oct 25 13:14:00 2009 +0100
+++ b/src/Pure/Tools/find_consts.ML	Sun Oct 25 13:20:31 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 13:14:00 2009 +0100
+++ b/src/Pure/consts.ML	Sun Oct 25 13:20:31 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 13:14:00 2009 +0100
+++ b/src/Pure/display.ML	Sun Oct 25 13:20:31 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))));
 

--- a/src/Pure/sign.ML	Sun Oct 25 13:14:00 2009 +0100
+++ b/src/Pure/sign.ML	Sun Oct 25 13:20:31 2009 +0100
@@ -125,6 +125,7 @@
   val parent_path: theory -> theory
   val mandatory_path: string -> theory -> theory
   val local_path: theory -> theory
+  val conceal: theory -> theory
   val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
@@ -618,6 +619,8 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
+val conceal = map_naming Name_Space.conceal;
+
 val restore_naming = map_naming o K o naming_of;