src/Pure/General/symbol.ML
changeset 53016 fa9c38891cf2
parent 52920 4539e4a06339
child 53198 06b096cf89ca
--- a/src/Pure/General/symbol.ML	Tue Aug 13 16:25:47 2013 +0200
+++ b/src/Pure/General/symbol.ML	Tue Aug 13 17:26:22 2013 +0200
@@ -516,7 +516,8 @@
 (* bump string -- treat as base 26 or base 1 numbers *)
 
 fun symbolic_end (_ :: "\\<^sub>" :: _) = true
-  | symbolic_end (_ :: "\\<^isub>" :: _) = true
+  | symbolic_end (_ :: "\\<^isub>" :: _) = true  (*legacy*)
+  | symbolic_end (_ :: "\\<^isup>" :: _) = true  (*legacy*)
   | symbolic_end (s :: _) = is_symbolic s
   | symbolic_end [] = false;