# HG changeset patch
# User wenzelm
# Date 1393084682 -3600
# Node ID 4612c450b59c1d3609c854dfbde96f4cf848b17b
# Parent  6e97c17665005dfaa397d304dc40d406bccf96cc
tuned signature;

diff -r 6e97c1766500 -r 4612c450b59c src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Sat Feb 22 16:16:21 2014 +0100
+++ b/src/Pure/General/long_name.ML	Sat Feb 22 16:58:02 2014 +0100
@@ -8,6 +8,8 @@
 sig
   val separator: string
   val is_qualified: string -> bool
+  val hidden: string -> string
+  val is_hidden: string -> bool
   val implode: string list -> string
   val explode: string -> string list
   val append: string -> string -> string
@@ -23,6 +25,9 @@
 val separator = ".";
 val is_qualified = exists_string (fn s => s = separator);
 
+fun hidden name = "??." ^ name;
+val is_hidden = String.isPrefix "??.";
+
 val implode = space_implode separator;
 val explode = space_explode separator;
 
diff -r 6e97c1766500 -r 4612c450b59c src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sat Feb 22 16:16:21 2014 +0100
+++ b/src/Pure/General/name_space.ML	Sat Feb 22 16:58:02 2014 +0100
@@ -9,8 +9,6 @@
 
 signature NAME_SPACE =
 sig
-  val hidden: string -> string
-  val is_hidden: string -> bool
   type T
   val empty: string -> T
   val kind_of: T -> string
@@ -72,12 +70,6 @@
 
 (** name spaces **)
 
-(* hidden entries *)
-
-fun hidden name = "??." ^ name;
-val is_hidden = String.isPrefix "??.";
-
-
 (* datatype entry *)
 
 type entry =
@@ -147,7 +139,7 @@
   | SOME ([], []) => (xname, true)
   | SOME ([name], _) => (name, true)
   | SOME (name :: _, _) => (name, false)
-  | SOME ([], name' :: _) => (hidden name', true));
+  | SOME ([], name' :: _) => (Long_Name.hidden name', true));
 
 fun get_accesses (Name_Space {entries, ...}) name =
   (case Symtab.lookup entries name of
@@ -183,7 +175,7 @@
       let val (name', is_unique) = lookup space xname
       in name = name' andalso (not require_unique orelse is_unique) end;
 
-    fun ext [] = if valid false name then name else hidden name
+    fun ext [] = if valid false name then name else Long_Name.hidden name
       | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
   in
     if names_long then name
@@ -212,7 +204,7 @@
 fun hide fully name space =
   if not (Long_Name.is_qualified name) then
     error ("Attempt to hide global name " ^ quote name)
-  else if is_hidden name then
+  else if Long_Name.is_hidden name then
     error ("Attempt to hide hidden name " ^ quote name)
   else
     let val names = valid_accesses space name in
diff -r 6e97c1766500 -r 4612c450b59c src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Feb 22 16:16:21 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sat Feb 22 16:58:02 2014 +0100
@@ -359,7 +359,7 @@
 local
 
 val index_ord = option_ord (K EQUAL);
-val hidden_ord = bool_ord o pairself Name_Space.is_hidden;
+val hidden_ord = bool_ord o pairself Long_Name.is_hidden;
 val qual_ord = int_ord o pairself (length o Long_Name.explode);
 val txt_ord = int_ord o pairself size;