generalize the Vampire parser some more to cope with things like "{2, 3\}" seen in some proofs
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 16 15:12:17 2010 +0100
@@ -281,7 +281,7 @@
(**** 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> *)