# 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*)