changeset 41201 | 208bd47b6f29 |
parent 41146 | be78f4053bce |
child 41203 | 1393514094d7 |
--- 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> *)