--- a/src/Pure/Syntax/lexicon.ML Thu Aug 08 17:24:31 2013 +0200
+++ b/src/Pure/Syntax/lexicon.ML Thu Aug 08 17:36:14 2013 +0200
@@ -296,8 +296,6 @@
fun chop_idx [] ds = idxname [] ds
| chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
| chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
- | chop_idx (cs as (_ :: "\\<^sup>" :: _)) ds = idxname cs ds
- | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
| chop_idx (c :: cs) ds =
if Symbol.is_digit c then chop_idx cs (c :: ds)
else idxname (c :: cs) ds;