diff -r 39002438a79c -r e10e02de3e02 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Tue Nov 19 13:20:38 1996 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Tue Nov 19 13:21:02 1996 +0100
@@ -190,10 +190,8 @@
             let
               val (ch_name, cs') = (scan_id -- $$ "}" >> #1) cs
                 handle LEXICAL_ERROR => err "malformed symbolic char specification";
-              val c =
-                if ch_name mem SymbolFont.char_names then
-                  SymbolFont.char ch_name
-                else err ("unknown symbolic char name: " ^ quote ch_name);
+              val c = the (SymbolFont.char ch_name)
+                handle OPTION _ => err ("unknown symbolic char name: " ^ quote ch_name);
             in (c, cs') end
         | scan_delim_char (chs as c :: cs) =
             if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)