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