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