| changeset 53198 | 06b096cf89ca |
| parent 53016 | fa9c38891cf2 |
| child 53403 | c09f4005d6bd |
--- a/src/Pure/General/symbol.ML Mon Aug 26 09:07:32 2013 +0200 +++ b/src/Pure/General/symbol.ML Mon Aug 26 10:33:16 2013 +0200 @@ -518,6 +518,7 @@ 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;