# HG changeset patch
# User wenzelm
# Date 1220357424 -7200
# Node ID a45ce1bae4e04f6ec946254937dc0a506306e773
# Parent  90adbbf0318798e53dcd1f8c956d42687bafebdf
added type binding -- generic name bindings;

diff -r 90adbbf03187 -r a45ce1bae4e0 src/Pure/name.ML
--- a/src/Pure/name.ML	Tue Sep 02 14:10:19 2008 +0200
+++ b/src/Pure/name.ML	Tue Sep 02 14:10:24 2008 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Makarius
 
-Names of basic logical entities (variables etc.).
+Names of basic logical entities (variables etc.).  Generic name bindings.
 *)
 
 signature NAME =
@@ -28,6 +28,13 @@
   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 =
@@ -139,4 +146,19 @@
 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;