changeset 52616 | 3ac2878764f9 |
parent 52161 | 51eca565b153 |
child 52920 | 4539e4a06339 |
--- a/src/Pure/term.ML Fri Jul 12 13:12:21 2013 +0200 +++ b/src/Pure/term.ML Wed Jul 10 16:25:26 2013 +0200 @@ -980,6 +980,7 @@ (case rev (Symbol.explode x) of _ :: "\\<^sub>" :: _ => false | _ :: "\\<^isub>" :: _ => false + | _ :: "\\<^sup>" :: _ => false | _ :: "\\<^isup>" :: _ => false | c :: _ => Symbol.is_digit c | _ => true);