# HG changeset patch
# User wenzelm
# Date 855246317 -3600
# Node ID 690835a06cf29c5fda6274853e8aa33ec63b3fbf
# Parent  b6e37441acb8c97210d878f75affc794d0771daa
added string_of_vname' (treats neg. index as free);

diff -r b6e37441acb8 -r 690835a06cf2 src/Pure/Syntax/lexicon.ML
--- 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 **)