# HG changeset patch
# User blanchet
# Date 1292508737 -3600
# Node ID 208bd47b6f29ef4deeb1dd27a65038cb588b4bb2
# Parent  6cc9b6fd7f6f2a851b0faaffdf73d7d9181e3f3c
generalize the Vampire parser some more to cope with things like "{2, 3\}" seen in some proofs

diff -r 6cc9b6fd7f6f -r 208bd47b6f29 src/HOL/Tools/ATP/atp_proof.ML
--- 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> *)