changeset 54732 | b01bb3d09928 |
parent 53403 | c09f4005d6bd |
child 54734 | b91afc3aa3e6 |
--- a/src/Pure/General/symbol.ML Thu Dec 12 22:38:25 2013 +0100 +++ b/src/Pure/General/symbol.ML Thu Dec 12 22:56:28 2013 +0100 @@ -517,8 +517,6 @@ (* bump string -- treat as base 26 or base 1 numbers *) fun symbolic_end (_ :: "\\<^sub>" :: _) = true - | symbolic_end (_ :: "\\<^isub>" :: _) = true (*legacy*) - | symbolic_end (_ :: "\\<^isup>" :: _) = true (*legacy*) | symbolic_end ("'" :: ss) = symbolic_end ss | symbolic_end (s :: _) = is_symbolic s | symbolic_end [] = false;