src/Pure/Syntax/lexicon.ML
changeset 1143 0dfb8b437f5d
parent 550 353eea6ec232
child 1507 f600215b6ea7
--- 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;