diff -r 392c69bdb170 -r 7b6629037127 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -505,6 +505,7 @@
     s
   else
     s |> no_qualifiers
+      |> perhaps (try (unprefix "'"))
       |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
       |> (fn s =>
              if size s > max_readable_name_size then
@@ -528,7 +529,7 @@
         fun add j =
           let
             val nice_name =
-              nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j)
+              nice_prefix ^ (if j = 0 then "" else string_of_int j)
           in
             case Symtab.lookup (snd the_pool) nice_name of
               SOME full_name' =>