# HG changeset patch
# User wenzelm
# Date 849109257 -3600
# Node ID 2888b4c1db7f1bf5b77c68afa6c035a1d780c0a4
# Parent  95b615550b8b45a775989cbddaebb608d4c8a6bd
changed symbolic char syntax to \<NAME>

diff -r 95b615550b8b -r 2888b4c1db7f src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Nov 27 16:40:23 1996 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Nov 27 16:40:57 1996 +0100
@@ -186,9 +186,9 @@
       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) =
+        | scan_delim_char ("\\" :: "<" :: cs) =
             let
-              val (ch_name, cs') = (scan_id -- $$ "}" >> #1) cs
+              val (ch_name, cs') = (scan_id -- $$ ">" >> #1) cs
                 handle LEXICAL_ERROR => err "malformed symbolic char specification";
               val c = the (SymbolFont.char ch_name)
                 handle OPTION _ => err ("unknown symbolic char name: " ^ quote ch_name);