--- 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
--- 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