# HG changeset patch
# User blanchet
# Date 1376380675 -7200
# Node ID dd28fbc5cecb5617fefd298927559210902913a2
# Parent  abd760a19e22ac49a06ac664738b45cd942ab604
more robust parsing of Vampire proofs with "introduced" names

diff -r abd760a19e22 -r dd28fbc5cecb src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Aug 12 23:36:43 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 13 09:57:55 2013 +0200
@@ -255,7 +255,8 @@
    --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
    -- parse_dependencies --| $$ "]" --| $$ ")") x
 and skip_introduced x =
-  (Scan.this_string "introduced" |-- $$ "(" |-- skip_term --| $$ ")") x
+  (Scan.this_string "introduced" |-- $$ "(" |-- skip_term
+   -- Scan.repeat ($$ "," |-- skip_term) --| $$ ")") x
 and parse_source x =
   (parse_file_source >> File_Source
    || parse_inference_source >> Inference_Source