more robust parsing of Vampire proofs with "introduced" names

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