changeset 54732 | b01bb3d09928 |
parent 53016 | fa9c38891cf2 |
child 56241 | 029246729dc0 |
--- a/src/Pure/term.ML Thu Dec 12 22:38:25 2013 +0100 +++ b/src/Pure/term.ML Thu Dec 12 22:56:28 2013 +0100 @@ -979,8 +979,6 @@ val dot = (case rev (Symbol.explode x) of _ :: "\\<^sub>" :: _ => false - | _ :: "\\<^isub>" :: _ => false (*legacy*) - | _ :: "\\<^isup>" :: _ => false (*legacy*) | c :: _ => Symbol.is_digit c | _ => true); in