| changeset 3769 | 931c336b0707 |
| parent 3761 | d99d93d46ca5 |
| child 3786 | d5655489867c |
--- a/src/Pure/name_space.ML Wed Oct 01 18:13:41 1997 +0200 +++ b/src/Pure/name_space.ML Wed Oct 01 18:19:18 1997 +0200 @@ -11,6 +11,7 @@ signature NAME_SPACE = sig + val separator: string (*single char!*) val unpack: string -> string list val pack: string list -> string val qualified: string -> bool