Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minor tuning;
authorwenzelm
Tue, 19 Nov 1996 13:21:02 +0100
changeset 2209 e10e02de3e02
parent 2208 39002438a79c
child 2210 8369f3f4bb4f
minor tuning;
src/Pure/Syntax/syn_ext.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle