# HG changeset patch
# User blanchet
# Date 1387221853 -3600
# Node ID 0e354ef1b16794e55c2fd8e41f96a489b47dbd68
# Parent  3d6ac2f68bf329c7a30910cdec9648a5280e2cd7
reverse Skolem function arguments

diff -r 3d6ac2f68bf3 -r 0e354ef1b167 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Dec 16 17:58:31 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Dec 16 20:24:13 2013 +0100
@@ -174,7 +174,8 @@
 fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
   | loose_aconv (t, t') = t aconv t'
 
-val vampire_skolem_prefix = "sK"
+(* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse order. *)
+val rev_skolem_prefixes = ["skf", "sK"]
 
 (* First-order translation. No types are known for variables. "HOLogic.typeT"
    should allow them to be inferred. *)
@@ -268,9 +269,7 @@
               [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
             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
+              |> exists (fn pre => String.isPrefix pre s) rev_skolem_prefixes ? rev
             val ts = term_ts @ extra_ts
             val T =
               case opt_T of
diff -r 3d6ac2f68bf3 -r 0e354ef1b167 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 17:58:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 20:24:13 2013 +0100
@@ -130,8 +130,8 @@
 (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
    type information. *)
 fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines =
-    (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire)
-       internal facts or definitions. *)
+    (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
+       definitions. *)
     if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
        role = Hypothesis orelse is_arith_rule rule then
       line :: lines