--- 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' =>