src/Pure/sign.ML

   val inherit_naming: theory -> Proof.context -> Context.generic
   val full_name: theory -> binding -> string
   val full_name_path: theory -> string -> binding -> string
   val full_bname: theory -> bstring -> string
   val full_bname_path: theory -> string -> bstring -> string
+  val bind_name: theory -> binding -> string * Position.T
   val const_monomorphic: theory -> string -> bool
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
   val mk_const: theory -> string * typ list -> term
   val class_space: theory -> Name_Space.T

 fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
 
 fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
 fun full_bname_path thy path = full_name_path thy path o Binding.name;
 
+fun bind_name thy b = (full_name thy b, Binding.default_pos_of b);
+
 
 
 (** name spaces **)
 
 val class_space = Type.class_space o tsig_of;