# HG changeset patch # User wenzelm # Date 1237465579 -3600 # Node ID 7e839627b9e74e4ae83c2a71220c3e883b30fd45 # Parent b51811144ed4317faae62e2d2506165065405c92 Name.of_binding: proper full_name (with checks) before projecting base name; diff -r b51811144ed4 -r 7e839627b9e7 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 --