# HG changeset patch
# User wenzelm
# Date 893841926 -7200
# Node ID cbbc53963aaa28de5f4f8e2ee086e5ec946f00e4
# Parent  050481f41e28d6d67d8a4a368dffe8beee8780ed
added append;

diff -r 050481f41e28 -r cbbc53963aaa src/Pure/name_space.ML
--- 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;