tuned signature;
authorwenzelm
Thu, 12 Mar 2009 11:07:22 +0100
changeset 30464 a858ff86883b
parent 30463 f1cb00030d4f
child 30465 038839f111a1
tuned signature;
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