1.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Nov 19 13:20:38 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Nov 19 13:21:02 1996 +0100
     1.3 @@ -190,10 +190,8 @@
     1.4              let
     1.5                val (ch_name, cs') = (scan_id -- $$ "}" >> #1) cs
     1.6                  handle LEXICAL_ERROR => err "malformed symbolic char specification";
     1.7 -              val c =
     1.8 -                if ch_name mem SymbolFont.char_names then
     1.9 -                  SymbolFont.char ch_name
    1.10 -                else err ("unknown symbolic char name: " ^ quote ch_name);
    1.11 +              val c = the (SymbolFont.char ch_name)
    1.12 +                handle OPTION _ => err ("unknown symbolic char name: " ^ quote ch_name);
    1.13              in (c, cs') end
    1.14          | scan_delim_char (chs as c :: cs) =
    1.15              if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)