# HG changeset patch
# User wenzelm
# Date 1236852442 -3600
# Node ID a858ff86883b5afbc0194226b1d20996271b4678
# Parent  f1cb00030d4f4fbac4e0667c94396b10bee7e9d1
tuned signature;

diff -r f1cb00030d4f -r a858ff86883b src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Thu Mar 12 00:02:30 2009 +0100
+++ b/src/Pure/General/binding.ML	Thu Mar 12 11:07:22 2009 +0100
@@ -14,7 +14,7 @@
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
   val name: bstring -> binding
-  val name_of: binding -> string
+  val name_of: binding -> bstring
   val map_name: (bstring -> bstring) -> binding -> binding
   val prefix_name: string -> binding -> binding
   val suffix_name: string -> binding -> binding
@@ -22,8 +22,8 @@
   val empty: binding
   val is_empty: binding -> bool
   val qualify: bool -> string -> binding -> binding
-  val qualified_name: bstring -> binding
-  val qualified_name_of: binding -> bstring
+  val qualified_name: string -> binding
+  val qualified_name_of: binding -> string
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding