src/Pure/Syntax/lexicon.ML

--- a/src/Pure/Syntax/lexicon.ML	Sat Jul 10 21:38:30 1999 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sat Jul 10 21:40:14 1999 +0200
@@ -108,7 +108,7 @@
 fun string_of_vname (x, i) =
   let
     val si = string_of_int i;
-    val dot = Symbol.is_digit (last_elem (Symbol.explode x)) handle _ => true;
+    val dot = if_none (try (Symbol.is_digit o last_elem o Symbol.explode) x) true;
   in
     if dot then "?" ^ x ^ "." ^ si
     else if i = 0 then "?" ^ x