changeset 59058 | a78612c67ec0 |
parent 58412 | f65f11f4854c |
child 61476 | 1884c40f1539 |
--- a/src/HOL/Tools/ATP/atp_satallax.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_satallax.ML Wed Nov 26 20:05:34 2014 +0100 @@ -426,7 +426,7 @@ | NONE => tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |> parse_proof local_prover problem - |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1))) + |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1))) |> local_prover = zipperpositionN ? rev) end;