diff -r 0271fda2a83a -r 30aaab778416 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Jun 08 16:20:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Jun 08 16:20:19 2011 +0200
@@ -351,9 +351,8 @@
       val (n, phis) = phi |> try (clausify_formula true) |> these |> `length
     in
       map2 (fn phi => fn j =>
-               Formula (ident ^
-                        (if n > 1 then "_cls" ^ string_of_int j else ""),
-                        kind, phi, source, info))
+               Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source,
+                        info))
            phis (1 upto n)
     end
   | clausify_formula_line _ = []