# HG changeset patch
# User wenzelm
# Date 1377505996 -7200
# Node ID 06b096cf89ca6acc36a109e5694497d3f2069aa8
# Parent  6c5e7143e1f65695a807a687a57a345e24969091
ignore trailing primes, e.g. rename \<alpha>' to \<alpha>'' instead of \<alpha>'a;

diff -r 6c5e7143e1f6 -r 06b096cf89ca src/Pure/General/symbol.ML
--- 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;