src/Pure/General/long_name.ML

 signature LONG_NAME =
 sig
   val separator: string
   val is_qualified: string -> bool
   val hidden: string -> string
-  val is_hidden: string -> bool
+  val dest_hidden: string -> string option
   val localN: string
-  val is_local: string -> bool
+  val dest_local: string -> string option
   val implode: string list -> string
   val explode: string -> string list
   val append: string -> string -> string
   val qualification: string -> int
   val qualify: string -> string -> string

 
 val separator = ".";
 
 val is_qualified = exists_string (fn s => s = separator);
 
-fun hidden name = "??." ^ name;
-val is_hidden = String.isPrefix "??.";
+val hidden = prefix "??.";
+val dest_hidden = try (unprefix "??.");
 
 val localN = "local";
-val is_local = String.isPrefix "local.";
+val dest_local = try (unprefix "local.");
 
 val implode = space_implode separator;
 val explode = space_explode separator;
 
 fun append name1 "" = name1