# HG changeset patch
# User blanchet
# Date 1504007774 -7200
# Node ID 3e838cf5e80ce95d4b7d05504f431007104243fe
# Parent  a90dbf19f573a2084875d000e39c2a297f341b99
improved Vampire proof parser

diff -r a90dbf19f573 -r 3e838cf5e80c src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 29 12:05:00 2017 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 29 13:56:14 2017 +0200
@@ -347,10 +347,13 @@
     || (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") [])
         -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
        >> AType)
-   -- Scan.option ($$ tptp_fun_type |-- parse_type)
+   -- Scan.option (($$ tptp_fun_type || $$ tptp_product_type) -- parse_type)
   >> (fn (a, NONE) => a
-       | (a, SOME b) => AFun (a, b))) x
-and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
+       | (a, SOME (fun_or_product, b)) =>
+         if fun_or_product = tptp_fun_type then AFun (a, b)
+         else AType ((tptp_product_type, []), [a, b]))) x
+and parse_types x =
+  (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
 
 (* We currently half ignore types. *)
 fun parse_optional_type_signature x =
diff -r a90dbf19f573 -r 3e838cf5e80c src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 29 12:05:00 2017 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 29 13:56:14 2017 +0200
@@ -717,7 +717,7 @@
   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
     (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
 val remote_vampire =
-  remotify_atp vampire "Vampire" ["4.2", "4.0"]
+  remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
     (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture