# HG changeset patch
# User wenzelm
# Date 1353958180 -3600
# Node ID b89b57bf4cf2defd14b545ce85dfb80adab2de2e
# Parent  c97c5c34fb1de09141788e42cf397f5894846561
tuned;

diff -r c97c5c34fb1d -r b89b57bf4cf2 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Nov 26 20:09:51 2012 +0100
+++ b/src/Pure/General/symbol.ML	Mon Nov 26 20:29:40 2012 +0100
@@ -230,147 +230,149 @@
 datatype kind = Letter | Digit | Quasi | Blank | Other;
 
 local
-  val symbol_kinds = Symtab.make
-   [("\\<A>", Letter),
-    ("\\<B>", Letter),
-    ("\\<C>", Letter),
-    ("\\<D>", Letter),
-    ("\\<E>", Letter),
-    ("\\<F>", Letter),
-    ("\\<G>", Letter),
-    ("\\<H>", Letter),
-    ("\\<I>", Letter),
-    ("\\<J>", Letter),
-    ("\\<K>", Letter),
-    ("\\<L>", Letter),
-    ("\\<M>", Letter),
-    ("\\<N>", Letter),
-    ("\\<O>", Letter),
-    ("\\<P>", Letter),
-    ("\\<Q>", Letter),
-    ("\\<R>", Letter),
-    ("\\<S>", Letter),
-    ("\\<T>", Letter),
-    ("\\<U>", Letter),
-    ("\\<V>", Letter),
-    ("\\<W>", Letter),
-    ("\\<X>", Letter),
-    ("\\<Y>", Letter),
-    ("\\<Z>", Letter),
-    ("\\<a>", Letter),
-    ("\\<b>", Letter),
-    ("\\<c>", Letter),
-    ("\\<d>", Letter),
-    ("\\<e>", Letter),
-    ("\\<f>", Letter),
-    ("\\<g>", Letter),
-    ("\\<h>", Letter),
-    ("\\<i>", Letter),
-    ("\\<j>", Letter),
-    ("\\<k>", Letter),
-    ("\\<l>", Letter),
-    ("\\<m>", Letter),
-    ("\\<n>", Letter),
-    ("\\<o>", Letter),
-    ("\\<p>", Letter),
-    ("\\<q>", Letter),
-    ("\\<r>", Letter),
-    ("\\<s>", Letter),
-    ("\\<t>", Letter),
-    ("\\<u>", Letter),
-    ("\\<v>", Letter),
-    ("\\<w>", Letter),
-    ("\\<x>", Letter),
-    ("\\<y>", Letter),
-    ("\\<z>", Letter),
-    ("\\<AA>", Letter),
-    ("\\<BB>", Letter),
-    ("\\<CC>", Letter),
-    ("\\<DD>", Letter),
-    ("\\<EE>", Letter),
-    ("\\<FF>", Letter),
-    ("\\<GG>", Letter),
-    ("\\<HH>", Letter),
-    ("\\<II>", Letter),
-    ("\\<JJ>", Letter),
-    ("\\<KK>", Letter),
-    ("\\<LL>", Letter),
-    ("\\<MM>", Letter),
-    ("\\<NN>", Letter),
-    ("\\<OO>", Letter),
-    ("\\<PP>", Letter),
-    ("\\<QQ>", Letter),
-    ("\\<RR>", Letter),
-    ("\\<SS>", Letter),
-    ("\\<TT>", Letter),
-    ("\\<UU>", Letter),
-    ("\\<VV>", Letter),
-    ("\\<WW>", Letter),
-    ("\\<XX>", Letter),
-    ("\\<YY>", Letter),
-    ("\\<ZZ>", Letter),
-    ("\\<aa>", Letter),
-    ("\\<bb>", Letter),
-    ("\\<cc>", Letter),
-    ("\\<dd>", Letter),
-    ("\\<ee>", Letter),
-    ("\\<ff>", Letter),
-    ("\\<gg>", Letter),
-    ("\\<hh>", Letter),
-    ("\\<ii>", Letter),
-    ("\\<jj>", Letter),
-    ("\\<kk>", Letter),
-    ("\\<ll>", Letter),
-    ("\\<mm>", Letter),
-    ("\\<nn>", Letter),
-    ("\\<oo>", Letter),
-    ("\\<pp>", Letter),
-    ("\\<qq>", Letter),
-    ("\\<rr>", Letter),
-    ("\\<ss>", Letter),
-    ("\\<tt>", Letter),
-    ("\\<uu>", Letter),
-    ("\\<vv>", Letter),
-    ("\\<ww>", Letter),
-    ("\\<xx>", Letter),
-    ("\\<yy>", Letter),
-    ("\\<zz>", Letter),
-    ("\\<alpha>", Letter),
-    ("\\<beta>", Letter),
-    ("\\<gamma>", Letter),
-    ("\\<delta>", Letter),
-    ("\\<epsilon>", Letter),
-    ("\\<zeta>", Letter),
-    ("\\<eta>", Letter),
-    ("\\<theta>", Letter),
-    ("\\<iota>", Letter),
-    ("\\<kappa>", Letter),
-    ("\\<lambda>", Other),      (*sic!*)
-    ("\\<mu>", Letter),
-    ("\\<nu>", Letter),
-    ("\\<xi>", Letter),
-    ("\\<pi>", Letter),
-    ("\\<rho>", Letter),
-    ("\\<sigma>", Letter),
-    ("\\<tau>", Letter),
-    ("\\<upsilon>", Letter),
-    ("\\<phi>", Letter),
-    ("\\<chi>", Letter),
-    ("\\<psi>", Letter),
-    ("\\<omega>", Letter),
-    ("\\<Gamma>", Letter),
-    ("\\<Delta>", Letter),
-    ("\\<Theta>", Letter),
-    ("\\<Lambda>", Letter),
-    ("\\<Xi>", Letter),
-    ("\\<Pi>", Letter),
-    ("\\<Sigma>", Letter),
-    ("\\<Upsilon>", Letter),
-    ("\\<Phi>", Letter),
-    ("\\<Psi>", Letter),
-    ("\\<Omega>", Letter),
-    ("\\<^isub>", Letter),
-    ("\\<^isup>", Letter)];
+  val letter_symbols =
+    Symtab.make_set [
+      "\\<A>",
+      "\\<B>",
+      "\\<C>",
+      "\\<D>",
+      "\\<E>",
+      "\\<F>",
+      "\\<G>",
+      "\\<H>",
+      "\\<I>",
+      "\\<J>",
+      "\\<K>",
+      "\\<L>",
+      "\\<M>",
+      "\\<N>",
+      "\\<O>",
+      "\\<P>",
+      "\\<Q>",
+      "\\<R>",
+      "\\<S>",
+      "\\<T>",
+      "\\<U>",
+      "\\<V>",
+      "\\<W>",
+      "\\<X>",
+      "\\<Y>",
+      "\\<Z>",
+      "\\<a>",
+      "\\<b>",
+      "\\<c>",
+      "\\<d>",
+      "\\<e>",
+      "\\<f>",
+      "\\<g>",
+      "\\<h>",
+      "\\<i>",
+      "\\<j>",
+      "\\<k>",
+      "\\<l>",
+      "\\<m>",
+      "\\<n>",
+      "\\<o>",
+      "\\<p>",
+      "\\<q>",
+      "\\<r>",
+      "\\<s>",
+      "\\<t>",
+      "\\<u>",
+      "\\<v>",
+      "\\<w>",
+      "\\<x>",
+      "\\<y>",
+      "\\<z>",
+      "\\<AA>",
+      "\\<BB>",
+      "\\<CC>",
+      "\\<DD>",
+      "\\<EE>",
+      "\\<FF>",
+      "\\<GG>",
+      "\\<HH>",
+      "\\<II>",
+      "\\<JJ>",
+      "\\<KK>",
+      "\\<LL>",
+      "\\<MM>",
+      "\\<NN>",
+      "\\<OO>",
+      "\\<PP>",
+      "\\<QQ>",
+      "\\<RR>",
+      "\\<SS>",
+      "\\<TT>",
+      "\\<UU>",
+      "\\<VV>",
+      "\\<WW>",
+      "\\<XX>",
+      "\\<YY>",
+      "\\<ZZ>",
+      "\\<aa>",
+      "\\<bb>",
+      "\\<cc>",
+      "\\<dd>",
+      "\\<ee>",
+      "\\<ff>",
+      "\\<gg>",
+      "\\<hh>",
+      "\\<ii>",
+      "\\<jj>",
+      "\\<kk>",
+      "\\<ll>",
+      "\\<mm>",
+      "\\<nn>",
+      "\\<oo>",
+      "\\<pp>",
+      "\\<qq>",
+      "\\<rr>",
+      "\\<ss>",
+      "\\<tt>",
+      "\\<uu>",
+      "\\<vv>",
+      "\\<ww>",
+      "\\<xx>",
+      "\\<yy>",
+      "\\<zz>",
+      "\\<alpha>",
+      "\\<beta>",
+      "\\<gamma>",
+      "\\<delta>",
+      "\\<epsilon>",
+      "\\<zeta>",
+      "\\<eta>",
+      "\\<theta>",
+      "\\<iota>",
+      "\\<kappa>",
+      (*"\\<lambda>", sic!*)
+      "\\<mu>",
+      "\\<nu>",
+      "\\<xi>",
+      "\\<pi>",
+      "\\<rho>",
+      "\\<sigma>",
+      "\\<tau>",
+      "\\<upsilon>",
+      "\\<phi>",
+      "\\<chi>",
+      "\\<psi>",
+      "\\<omega>",
+      "\\<Gamma>",
+      "\\<Delta>",
+      "\\<Theta>",
+      "\\<Lambda>",
+      "\\<Xi>",
+      "\\<Pi>",
+      "\\<Sigma>",
+      "\\<Upsilon>",
+      "\\<Phi>",
+      "\\<Psi>",
+      "\\<Omega>",
+      "\\<^isub>",
+      "\\<^isup>"
+    ];
 in
   fun kind s =
     if is_ascii_letter s then Letter
@@ -378,7 +380,8 @@
     else if is_ascii_quasi s then Quasi
     else if is_ascii_blank s then Blank
     else if is_char s then Other
-    else the_default Other (Symtab.lookup symbol_kinds s);
+    else if Symtab.defined letter_symbols s then Letter
+    else Other;
 end;
 
 fun is_letter s = kind s = Letter;