--- a/src/Pure/General/long_name.ML Sat Mar 15 11:59:18 2014 +0100
+++ b/src/Pure/General/long_name.ML Sat Mar 15 12:51:14 2014 +0100
@@ -10,6 +10,8 @@
val is_qualified: string -> bool
val hidden: string -> string
val is_hidden: string -> bool
+ val localN: string
+ val is_local: string -> bool
val implode: string list -> string
val explode: string -> string list
val append: string -> string -> string
@@ -29,6 +31,9 @@
fun hidden name = "??." ^ name;
val is_hidden = String.isPrefix "??.";
+val localN = "local";
+val is_local = String.isPrefix "local.";
+
val implode = space_implode separator;
val explode = space_explode separator;