# HG changeset patch
# User wenzelm
# Date 1236457117 -3600
# Node ID 51d488f3dd7200972385c4de6fb624cc990a24f5
# Parent  eb189f7e43a1aaee2998270c0dc4851feb42e1e1
added prefix_name, suffix_name;
added eq_name;
added opaque signature constraint to prevent accidental equality test;

diff -r eb189f7e43a1 -r 51d488f3dd72 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Sat Mar 07 12:07:30 2009 +0100
+++ b/src/Pure/General/binding.ML	Sat Mar 07 21:18:37 2009 +0100
@@ -17,6 +17,9 @@
   val name: bstring -> binding
   val name_of: binding -> string
   val map_name: (bstring -> bstring) -> binding -> binding
+  val prefix_name: string -> binding -> binding
+  val suffix_name: string -> binding -> binding
+  val eq_name: binding * binding -> bool
   val empty: binding
   val is_empty: binding -> bool
   val qualify: bool -> string -> binding -> binding
@@ -25,7 +28,7 @@
   val prefix: bool -> string -> binding -> binding
 end;
 
-structure Binding: BINDING =
+structure Binding:> BINDING =
 struct
 
 (** representation **)
@@ -64,7 +67,11 @@
 fun pos_of (Binding {pos, ...}) = pos;
 fun name_of (Binding {name, ...}) = name;
 
+fun eq_name (b, b') = name_of b = name_of b';
+
 fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos));
+val prefix_name = map_name o prefix;
+val suffix_name = map_name o suffix;
 
 val empty = name "";
 fun is_empty b = name_of b = "";