Now string_of_vname checks for the empty variable name,
authorlcp
Tue, 06 Jun 1995 10:33:32 +0200
changeset 1143 0dfb8b437f5d
parent 1142 eb0e2ff8f032
child 1144 5a62ecf80126
Now string_of_vname checks for the empty variable name, catching the exception LIST.
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;