# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID 84b134118616676e9f68409577491339dd982865
# Parent  6321d0dc3d72cf7a6e991eda6c08327da7463153
avoid trailing digits for SNARK (type) names -- grr...

diff -r 6321d0dc3d72 -r 84b134118616 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:25 2011 +0200
@@ -176,11 +176,17 @@
   else
     s |> no_qualifiers
       |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
-      |> (fn s => if size s > max_readable_name_length then
-                    String.substring (s, 0, max_readable_name_length) ^ "_" ^
-                    Word.toString (hashw_string (full_name, 0w0))
-                  else
-                    s)
+         (* SNARK doesn't like sort (type) names that end with digits. We make
+            an effort to avoid this here. *)
+      |> (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) ^
+               Word.toString (hashw_string (full_name, 0w0)) ^
+               String.extract (s, max_readable_name_length div 2 - 4, NONE)
+             else
+               s)
       |> (fn s => if member (op =) reserved_nice_names s then full_name else s)
 
 fun nice_name (full_name, _) NONE = (full_name, NONE)