src/Pure/name_space.ML
changeset 3769 931c336b0707
parent 3761 d99d93d46ca5
child 3786 d5655489867c
equal deleted inserted replaced
3768:67f4ac759100 3769:931c336b0707
     9 are implicitely considered to be declared outermost.
     9 are implicitely considered to be declared outermost.
    10 *)
    10 *)
    11 
    11 
    12 signature NAME_SPACE =
    12 signature NAME_SPACE =
    13 sig
    13 sig
       
    14   val separator: string		(*single char!*)
    14   val unpack: string -> string list
    15   val unpack: string -> string list
    15   val pack: string list -> string
    16   val pack: string list -> string
    16   val qualified: string -> bool
    17   val qualified: string -> bool
    17   type T
    18   type T
    18   val dest: T -> string list
    19   val dest: T -> string list