changeset 50242 | 56b9c792a98b |
parent 49674 | dbadb4d03cbc |
child 52161 | 51eca565b153 |
--- a/src/Pure/term.ML Tue Nov 27 13:22:29 2012 +0100 +++ b/src/Pure/term.ML Tue Nov 27 19:22:36 2012 +0100 @@ -981,7 +981,8 @@ val idx = string_of_int i; val dot = (case rev (Symbol.explode x) of - _ :: "\\<^isub>" :: _ => false + _ :: "\\<^sub>" :: _ => false + | _ :: "\\<^isub>" :: _ => false | _ :: "\\<^isup>" :: _ => false | c :: _ => Symbol.is_digit c | _ => true);