# HG changeset patch
# User wenzelm
# Date 1683462341 -7200
# Node ID c1b8fdd6588ac232110e61559a4e7b09236fe309
# Parent  a35b9a01b5a9144b9baf9b74b59b37c46cbffae3
tuned comments;

diff -r a35b9a01b5a9 -r c1b8fdd6588a src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun May 07 14:24:22 2023 +0200
+++ b/src/Pure/General/name_space.ML	Sun May 07 14:25:41 2023 +0200
@@ -1,11 +1,10 @@
 (*  Title:      Pure/General/name_space.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Generic name spaces with declared and hidden entries; no support for
-absolute addressing.
+Generic name spaces with authentic declarations, hidden names and aliases.
 *)
 
-type xstring = string;    (*external names*)
+type xstring = string;    (*external names with partial qualification*)
 
 signature NAME_SPACE =
 sig