src/Pure/Syntax/syn_ext.ML

       fun is_meta c = c mem ["(", ")", "/", "_"];
 
       fun scan_delim_char ("'" :: c :: cs) =
             if is_blank c then raise LEXICAL_ERROR else (c, cs)
         | scan_delim_char ["'"] = err "trailing escape character"
+        | scan_delim_char ("\\" :: "{" :: cs) =
+            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);
+            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)
         | scan_delim_char [] = raise LEXICAL_ERROR;
 
       val scan_sym =