--- a/src/Pure/name_space.ML Wed Apr 29 11:24:58 1998 +0200
+++ b/src/Pure/name_space.ML Wed Apr 29 11:25:26 1998 +0200
@@ -11,7 +11,8 @@
signature NAME_SPACE =
sig
- val separator: string (*single char*)
+ val separator: string (*single char!*)
+ val append: string -> string -> string
val unpack: string -> string list
val pack: string list -> string
val base: string -> string
@@ -42,6 +43,8 @@
val separator = ".";
+fun append name1 name2 = name1 ^ separator ^ name2;
+
val unpack = space_explode separator;
val pack = space_implode separator;