src/Pure/Syntax/lexicon.ML
changeset 2583 690835a06cf2
parent 2363 963285471dc5
child 3828 f6a7ca242dc2
--- a/src/Pure/Syntax/lexicon.ML	Thu Feb 06 17:24:05 1997 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Thu Feb 06 17:25:17 1997 +0100
@@ -43,6 +43,7 @@
   sig
   val is_identifier: string -> bool
   val string_of_vname: indexname -> string
+  val string_of_vname': indexname -> string
   val scan_varname: string list -> indexname * string list
   val scan_var: string -> term
   val const: string -> term
@@ -114,6 +115,9 @@
     handle LIST _ => "?NULL_VARIABLE." ^ si
   end;
 
+fun string_of_vname' (xi as (x, i)) =
+  if i < 0 then x else string_of_vname xi;
+
 
 
 (** datatype token **)