# HG changeset patch
# User wenzelm
# Date 1236089347 -3600
# Node ID 894eb2034f021e259184f806902b50a8f9db761d
# Parent  0300b7420b07b78a5814c116d4066b5b418fc1f1
renamed Binding.display to Binding.str_of, which is slightly more canonical;
tuned signature;

diff -r 0300b7420b07 -r 894eb2034f02 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue Mar 03 14:54:12 2009 +0100
+++ b/src/Pure/General/binding.ML	Tue Mar 03 15:09:07 2009 +0100
@@ -7,7 +7,10 @@
 
 signature BINDING =
 sig
+  val separator: string
+  val is_qualified: string -> bool
   type binding
+  val str_of: binding -> string
   val name_pos: string * Position.T -> binding
   val name: string -> binding
   val empty: binding
@@ -19,12 +22,9 @@
   val base_name: binding -> string
   val pos_of: binding -> Position.T
   val dest: binding -> (string * bool) list * string
-  val separator: string
-  val is_qualified: string -> bool
-  val display: binding -> string
 end;
 
-structure Binding : BINDING =
+structure Binding: BINDING =
 struct
 
 (** qualification **)
@@ -43,6 +43,13 @@
 datatype binding = Binding of ((string * bool) list * string) * Position.T;
   (* (prefix components (with mandatory flag), base name, position) *)
 
+fun str_of (Binding ((prefix, name), _)) =
+  let
+    fun mk_prefix (prfx, true) = prfx
+      | mk_prefix (prfx, false) = enclose "(" ")" prfx
+  in space_implode "." (map mk_prefix prefix) ^ ":" ^ name end;
+
+
 fun name_pos (name, pos) = Binding (([], name), pos);
 fun name name = name_pos (name, Position.none);
 val empty = name "";
@@ -70,12 +77,6 @@
 fun pos_of (Binding (_, pos)) = pos;
 fun dest (Binding (prefix_name, _)) = prefix_name;
 
-fun display (Binding ((prefix, name), _)) =
-  let
-    fun mk_prefix (prfx, true) = prfx
-      | mk_prefix (prfx, false) = enclose "(" ")" prfx
-  in space_implode "." (map mk_prefix prefix) ^ ":" ^ name end;
-
 end;
 
 type binding = Binding.binding;