more specific exn;

--- 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

--- a/src/Pure/Syntax/parser.ML	Sat Jul 10 21:38:30 1999 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Jul 10 21:40:14 1999 +0200
@@ -193,7 +193,7 @@
                       (*existing productions whose lookahead may depend on l*)
                       val tk_prods =
                         assocs nt_prods
-                               (Some (hd l_starts  handle Hd => UnknownStart));
+                               (Some (hd l_starts  handle LIST _ => UnknownStart));
 
                       (*add_lambda is true if an existing production of the nt
                         produces lambda due to the new lambda NT l*)