# HG changeset patch
# User wenzelm
# Date 1086800181 -7200
# Node ID 944087c009328c8766d0183c8b4e68cafded0c89
# Parent  c77fda9b6cf0599a5b39fb181809d943294c668d
tuned;

diff -r c77fda9b6cf0 -r 944087c00932 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Jun 09 18:56:09 2004 +0200
+++ b/src/Pure/General/symbol.ML	Wed Jun 09 18:56:21 2004 +0200
@@ -427,13 +427,13 @@
 
 (* bump string -- treat as base 26 or base 1 numbers *)
 
-fun ends_symbolic (_ :: "\\<^isup>" :: _) = true
-  | ends_symbolic (_ :: "\\<^isub>" :: _) = true
-  | ends_symbolic (s :: _) = is_symbolic s
-  | ends_symbolic [] = false;
+fun symbolic_end (_ :: "\\<^isup>" :: _) = true
+  | symbolic_end (_ :: "\\<^isub>" :: _) = true
+  | symbolic_end (s :: _) = is_symbolic s
+  | symbolic_end [] = false;
 
 fun bump_init str =
-  if ends_symbolic (rev (sym_explode str)) then str ^ "'"
+  if symbolic_end (rev (sym_explode str)) then str ^ "'"
   else str ^ "a";
 
 fun bump_string str =
@@ -446,7 +446,7 @@
           else "a" :: s :: ss;
 
     val (ss, qs) = apfst rev (Library.take_suffix is_quasi (sym_explode str));
-    val ss' = if ends_symbolic ss then "'" :: ss else bump ss;
+    val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   in implode (rev ss' @ qs) end;