# HG changeset patch
# User blanchet
# Date 1304441242 -7200
# Node ID 8d53e7945078bd911ddeab1167796becedcad41e
# Parent  8f5d5d71add0fe4dcba9fade708348e698cb1e6c
fixed long name truncation logic

diff -r 8f5d5d71add0 -r 8d53e7945078 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 03 18:04:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 03 18:47:22 2011 +0200
@@ -167,7 +167,7 @@
       | keep (c :: cs) = c :: keep cs
   in String.explode #> rev #> keep #> rev #> String.implode end
 
-val max_readable_name_length = 24
+val max_readable_name_size = 24
 
 (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
    problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
@@ -184,10 +184,11 @@
       |> (fn s => if Char.isDigit (String.sub (s, size s - 1)) then s ^ "_"
                   else s)
       |> (fn s =>
-             if size s > max_readable_name_length then
-               String.substring (s, 0, max_readable_name_length div 2 - 4) ^
+             if size s > max_readable_name_size then
+               String.substring (s, 0, max_readable_name_size div 2 - 4) ^
                Word.toString (hashw_string (full_name, 0w0)) ^
-               String.extract (s, max_readable_name_length div 2 + 4, NONE)
+               String.extract (s, size s - max_readable_name_size div 2 + 4,
+                               NONE)
              else
                s)
       |> (fn s => if member (op =) reserved_nice_names s then full_name else s)