changeset 4144 | 873489c611fc |
parent 3069 | de1f64558c01 |
--- a/src/Pure/Syntax/symbol_font.ML Wed Nov 05 11:40:23 1997 +0100 +++ b/src/Pure/Syntax/symbol_font.ML Wed Nov 05 11:40:51 1997 +0100 @@ -158,7 +158,7 @@ let val (name, cs') = (scan_id -- $$ ">" >> #1) cs handle LEXICAL_ERROR => error ("Malformed symbolic char specification: \"\\<" ^ implode cs ^ "\""); - val c = the (char name) handle OPTION _ + val c = the (char name) handle OPTION => error ("Unknown symbolic char name: " ^ quote name); in (c, cs') end | scan_symbol _ = raise LEXICAL_ERROR;