src/HOL/Tools/ATP/atp_satallax.ML
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;