src/Pure/name.ML

 (*  Title:      Pure/name.ML
     ID:         $Id$
     Author:     Makarius
 
-Names of basic logical entities (variables etc.).
+Names of basic logical entities (variables etc.).  Generic name bindings.
 *)
 
 signature NAME =
 sig
   val uu: string

   val names: context -> string -> 'a list -> (string * 'a) list
   val invent_list: string list -> string -> int -> string list
   val variants: string list -> context -> string list * context
   val variant_list: string list -> string list -> string list
   val variant: string list -> string -> string
+  type binding
+  val binding_pos: string * Position.T -> binding
+  val binding: string -> binding
+  val no_binding: binding
+  val name_of: binding -> string
+  val pos_of: binding -> Position.T
+  val map_name: (string -> string) -> binding -> binding
 end;
 
 structure Name: NAME =
 struct
 

   in (x' ^ replicate_string n "_", ctxt') end);
 
 fun variant_list used names = #1 (make_context used |> variants names);
 fun variant used = singleton (variant_list used);
 
+
+
+(** generic name bindings **)
+
+datatype binding = Binding of string * Position.T;
+
+val binding_pos = Binding;
+fun binding name = binding_pos (name, Position.none);
+val no_binding = binding "";
+
+fun name_of (Binding (name, _)) = name;
+fun pos_of (Binding (_, pos)) = pos;
+
+fun map_name f (Binding (name, pos)) = Binding (f name, pos);
+
 end;