# HG changeset patch
# User lcp
# Date 802427612 -7200
# Node ID 0dfb8b437f5d56041b6368feaa8d5627c4bb781a
# Parent  eb0e2ff8f032253288ba457329431201bdf495d6
Now string_of_vname checks for the empty variable name,
catching the exception LIST.

diff -r eb0e2ff8f032 -r 0dfb8b437f5d src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Jun 02 10:38:48 1995 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Jun 06 10:33:32 1995 +0200
@@ -109,9 +109,10 @@
   let
     val si = string_of_int i;
   in
-    if is_digit (last_elem (explode x)) then "?" ^ x ^ "." ^ si
-    else if i = 0 then "?" ^ x
-    else "?" ^ x ^ si
+    (if is_digit (last_elem (explode x)) then "?" ^ x ^ "." ^ si
+     else if i = 0 then "?" ^ x
+     else "?" ^ x ^ si)
+    handle LIST _ => "?NULL_VARIABLE." ^ si
   end;