fixed exception OPTION;
authorwenzelm
Wed Nov 05 11:40:51 1997 +0100 (1997-11-05)
changeset 4144873489c611fc
parent 4143 4bd5f4c05cf6
child 4145 ffb0c9670597
fixed exception OPTION;
src/Pure/Syntax/symbol_font.ML
     1.1 --- a/src/Pure/Syntax/symbol_font.ML	Wed Nov 05 11:40:23 1997 +0100
     1.2 +++ b/src/Pure/Syntax/symbol_font.ML	Wed Nov 05 11:40:51 1997 +0100
     1.3 @@ -158,7 +158,7 @@
     1.4          let
     1.5            val (name, cs') = (scan_id -- $$ ">" >> #1) cs handle LEXICAL_ERROR
     1.6              => error ("Malformed symbolic char specification: \"\\<" ^ implode cs ^ "\"");
     1.7 -          val c = the (char name) handle OPTION _
     1.8 +          val c = the (char name) handle OPTION
     1.9              => error ("Unknown symbolic char name: " ^ quote name);
    1.10          in (c, cs') end
    1.11      | scan_symbol _ = raise LEXICAL_ERROR;