Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuning ATP problem output
authorblanchet
Mon, 22 Aug 2011 15:02:45 +0200
changeset 44407 7b6629037127
parent 44406 392c69bdb170
child 44408 30ea62ab4f16
tuning ATP problem output
src/HOL/Tools/ATP/atp_problem.ML file | annotate | diff | comparison | revisions 
--- 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' =>
isabelle