| changeset 52920 | 4539e4a06339 |
| parent 52616 | 3ac2878764f9 |
| child 53016 | fa9c38891cf2 |
--- a/src/Pure/General/symbol.ML Thu Aug 08 17:24:31 2013 +0200 +++ b/src/Pure/General/symbol.ML Thu Aug 08 17:36:14 2013 +0200 @@ -517,8 +517,6 @@ fun symbolic_end (_ :: "\\<^sub>" :: _) = true | symbolic_end (_ :: "\\<^isub>" :: _) = true - | symbolic_end (_ :: "\\<^sup>" :: _) = true - | symbolic_end (_ :: "\\<^isup>" :: _) = true | symbolic_end (s :: _) = is_symbolic s | symbolic_end [] = false;