Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_problem.ML
changeset 43295 30aaab778416
parent 43224 97906dfd39b7
child 43422 dcbedaf6f80c 
--- 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 _ = []
isabelle