src/Pure/name.ML
changeset 30584 7e839627b9e7
parent 29006 abe0f11cfa4e
child 31013 69a476d6fea6
equal deleted inserted replaced
30583:b51811144ed4 30584:7e839627b9e7
     6 
     6 
     7 signature NAME =
     7 signature NAME =
     8 sig
     8 sig
     9   val uu: string
     9   val uu: string
    10   val aT: string
    10   val aT: string
       
    11   val of_binding: binding -> string
    11   val bound: int -> string
    12   val bound: int -> string
    12   val is_bound: string -> bool
    13   val is_bound: string -> bool
    13   val internal: string -> string
    14   val internal: string -> string
    14   val dest_internal: string -> string
    15   val dest_internal: string -> string
    15   val skolem: string -> string
    16   val skolem: string -> string
    38 val aT = "'a";
    39 val aT = "'a";
    39 
    40 
    40 
    41 
    41 
    42 
    42 (** special variable names **)
    43 (** special variable names **)
       
    44 
       
    45 (* checked binding *)
       
    46 
       
    47 val of_binding = Long_Name.base_name o NameSpace.full_name NameSpace.default_naming;
       
    48 
    43 
    49 
    44 (* encoded bounds *)
    50 (* encoded bounds *)
    45 
    51 
    46 (*names for numbered variables --
    52 (*names for numbered variables --
    47   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
    53   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)