# HG changeset patch
# User wenzelm
# Date 878726451 -3600
# Node ID 873489c611fccd604d32a1c83e3a8d292683cb96
# Parent  4bd5f4c05cf6ebff1ef29c5285b8ac3ecdff6c47
fixed exception OPTION;

diff -r 4bd5f4c05cf6 -r 873489c611fc src/Pure/Syntax/symbol_font.ML
--- a/src/Pure/Syntax/symbol_font.ML	Wed Nov 05 11:40:23 1997 +0100
+++ b/src/Pure/Syntax/symbol_font.ML	Wed Nov 05 11:40:51 1997 +0100
@@ -158,7 +158,7 @@
         let
           val (name, cs') = (scan_id -- $$ ">" >> #1) cs handle LEXICAL_ERROR
             => error ("Malformed symbolic char specification: \"\\<" ^ implode cs ^ "\"");
-          val c = the (char name) handle OPTION _
+          val c = the (char name) handle OPTION
             => error ("Unknown symbolic char name: " ^ quote name);
         in (c, cs') end
     | scan_symbol _ = raise LEXICAL_ERROR;