diff -r c7b71b55099b -r 9dd98edd48c2 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon May 02 22:52:15 2011 +0200
@@ -203,8 +203,9 @@
         val nice_prefix = readable_name full_name desired_name
         fun add j =
           let
-            val nice_name = nice_prefix ^
-                            (if j = 0 then "" else "_" ^ string_of_int j)
+            (* The trailing "_" is for SNARK (cf. comment above). *)
+            val nice_name =
+              nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j ^ "_")
           in
             case Symtab.lookup (snd the_pool) nice_name of
               SOME full_name' =>