src/HOL/Tools/ATP/atp_proof.ML

           end)
 
 (**** PARSING OF VAMPIRE OUTPUT ****)
 
 val parse_vampire_braced_stuff =
-  $$ "{" -- scan_general_id -- $$ "}"
+  $$ "{" -- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) -- $$ "}"
   -- Scan.option ($$ "(" |-- parse_vampire_detritus --| $$ ")")
 
 (* Syntax: <num>. <formula> <annotation> *)
 val parse_vampire_line =
   scan_general_id --| $$ "." -- parse_formula