# HG changeset patch
# User blanchet
# Date 1440699367 -7200
# Node ID aeb578badc1cb8dfd3bd8c71f4f27ddfd7beb727
# Parent  b09461b3bc057dbf2a5ee18571c137ba4854c0b9
robust handling of Vampire 4 proofs

diff -r b09461b3bc05 -r aeb578badc1c NEWS
--- a/NEWS	Thu Aug 27 20:10:40 2015 +0200
+++ b/NEWS	Thu Aug 27 20:16:07 2015 +0200
@@ -192,6 +192,7 @@
   - Proof reconstruction has been improved, to minimize the incidence of
     cases where Sledgehammer gives a proof that does not work.
   - Auto Sledgehammer now minimizes and preplays the results.
+  - Handle Vampire 4.0 proof output without raising exception.
 
 * Nitpick:
   - Removed "check_potential" and "check_genuine" options.
diff -r b09461b3bc05 -r aeb578badc1c src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Aug 27 20:10:40 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Aug 27 20:16:07 2015 +0200
@@ -404,7 +404,7 @@
 and parse_quantified_formula x =
   (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists)
    --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
-   >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x
+   >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, _), _) => (s, NONE)) ts, phi))) x
 
 val parse_tstp_extra_arguments =
   Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) dummy_inference