1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -505,6 +505,7 @@
     1.4      s
     1.5    else
     1.6      s |> no_qualifiers
     1.7 +      |> perhaps (try (unprefix "'"))
     1.8        |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0)))
     1.9        |> (fn s =>
    1.10               if size s > max_readable_name_size then
    1.11 @@ -528,7 +529,7 @@
    1.12          fun add j =
    1.13            let
    1.14              val nice_name =
    1.15 -              nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j)
    1.16 +              nice_prefix ^ (if j = 0 then "" else string_of_int j)
    1.17            in
    1.18              case Symtab.lookup (snd the_pool) nice_name of
    1.19                SOME full_name' =>