1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 03 18:04:05 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 03 18:47:22 2011 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4        | keep (c :: cs) = c :: keep cs
     1.5    in String.explode #> rev #> keep #> rev #> String.implode end
     1.6  
     1.7 -val max_readable_name_length = 24
     1.8 +val max_readable_name_size = 24
     1.9  
    1.10  (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
    1.11     problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
    1.12 @@ -184,10 +184,11 @@
    1.13        |> (fn s => if Char.isDigit (String.sub (s, size s - 1)) then s ^ "_"
    1.14                    else s)
    1.15        |> (fn s =>
    1.16 -             if size s > max_readable_name_length then
    1.17 -               String.substring (s, 0, max_readable_name_length div 2 - 4) ^
    1.18 +             if size s > max_readable_name_size then
    1.19 +               String.substring (s, 0, max_readable_name_size div 2 - 4) ^
    1.20                 Word.toString (hashw_string (full_name, 0w0)) ^
    1.21 -               String.extract (s, max_readable_name_length div 2 + 4, NONE)
    1.22 +               String.extract (s, size s - max_readable_name_size div 2 + 4,
    1.23 +                               NONE)
    1.24               else
    1.25                 s)
    1.26        |> (fn s => if member (op =) reserved_nice_names s then full_name else s)