src/Pure/General/long_name.ML
changeset 56162 ea6303e2261b
parent 56023 f252a315c26e
child 56800 b904ea8edd73
--- 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;