# HG changeset patch # User wenzelm # Date 878726451 -3600 # Node ID 873489c611fccd604d32a1c83e3a8d292683cb96 # Parent 4bd5f4c05cf6ebff1ef29c5285b8ac3ecdff6c47 fixed exception OPTION; diff -r 4bd5f4c05cf6 -r 873489c611fc src/Pure/Syntax/symbol_font.ML --- 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;