changeset 9120 | 04a46ceace35 |
parent 8806 | a202293db3f6 |
child 11829 | f252646080fc |
--- 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