# HG changeset patch
# User blanchet
# Date 1357222391 -3600
# Node ID 76a2e506c125b4f970912c1b1e950dbd156519b0
# Parent  70c2a6d513fd956533da53d1331d82176255acdc
swap Vampire's Skolem arguments to bring them in line with what E and metis's new skolemizer do (helps Isar proof reconstruction in some cases)

diff -r 70c2a6d513fd -r 76a2e506c125 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 03 14:41:05 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu Jan 03 15:13:11 2013 +0100
@@ -158,6 +158,8 @@
 
 fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
 
+val vampire_skolem_prefix = "sK"
+
 (* First-order translation. No types are known for variables. "HOLogic.typeT"
    should allow them to be inferred. *)
 fun term_from_atp ctxt textual sym_tab =
@@ -246,7 +248,11 @@
                end with a digit and "variant_frees" appends letters. *)
             fun fresh_up s =
               [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
-            val term_ts = map (do_term [] NONE) us
+            val term_ts =
+              map (do_term [] NONE) us
+              (* Vampire (2.6) passes arguments to Skolem functions in reverse
+                 order *)
+              |> String.isPrefix vampire_skolem_prefix s ? rev
             val ts = term_ts @ extra_ts
             val T =
               case opt_T of