author | wenzelm |
Sun, 25 Jun 2000 23:46:03 +0200 | |
changeset 9120 | 04a46ceace35 |
parent 9119 | 8ca79837b41b |
child 9121 | 25245986e667 |
--- a/src/Pure/General/name_space.ML Sun Jun 25 23:45:47 2000 +0200 +++ b/src/Pure/General/name_space.ML Sun Jun 25 23:46:03 2000 +0200 @@ -13,6 +13,7 @@ signature NAME_SPACE = sig val separator: string (*single char!*) + val hidden: string -> string val append: string -> string -> string val unpack: string -> string list val pack: string list -> string