src/Pure/name.ML

--- a/src/Pure/name.ML	Thu Mar 19 11:51:49 2009 +0100
+++ b/src/Pure/name.ML	Thu Mar 19 13:26:19 2009 +0100
@@ -8,6 +8,7 @@
 sig
   val uu: string
   val aT: string
+  val of_binding: binding -> string
   val bound: int -> string
   val is_bound: string -> bool
   val internal: string -> string
@@ -41,6 +42,11 @@
 
 (** special variable names **)
 
+(* checked binding *)
+
+val of_binding = Long_Name.base_name o NameSpace.full_name NameSpace.default_naming;
+
+
 (* encoded bounds *)
 
 (*names for numbered variables --