# HG changeset patch
# User wenzelm
# Date 931635614 -7200
# Node ID 3996436335294662be5aba3e0751c5ade438cc62
# Parent  4d404c52ca802d09245fb4df1b73b7dcc798e9df
more specific exn;

diff -r 4d404c52ca80 -r 399643633529 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
diff -r 4d404c52ca80 -r 399643633529 src/Pure/Syntax/parser.ML
--- 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*)