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;