src/Pure/term.ML
changeset 53016 fa9c38891cf2
parent 52920 4539e4a06339
child 54732 b01bb3d09928
--- a/src/Pure/term.ML	Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/term.ML	Tue Aug 13 17:26:22 2013 +0200
@@ -979,7 +979,8 @@
     val dot =
       (case rev (Symbol.explode x) of
         _ :: "\\<^sub>" :: _ => false
-      | _ :: "\\<^isub>" :: _ => false
+      | _ :: "\\<^isub>" :: _ => false  (*legacy*)
+      | _ :: "\\<^isup>" :: _ => false  (*legacy*)
       | c :: _ => Symbol.is_digit c
       | _ => true);
   in