ignore trailing primes, e.g. rename \<alpha>' to \<alpha>'' instead of \<alpha>'a;
--- 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;