# HG changeset patch
# User blanchet
# Date 1328890249 -3600
# Node ID 4989249a4b81747ce049ea547f600f6dc536fd1b
# Parent  7560930b2e06105324eadfb8613ade6a51ed006e
parse clauses generated from several formulas

diff -r 7560930b2e06 -r 4989249a4b81 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Feb 10 17:10:47 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Feb 10 17:10:49 2012 +0100
@@ -451,7 +451,7 @@
     -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
     -- parse_horn_clause --| $$ "."
     -- Scan.option (Scan.this_string "derived from formulae "
-                    |-- Scan.repeat scan_general_id)
+                    |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
   >> (fn ((((num, rule), deps), u), names) =>
          Inference ((num, resolve_spass_num names spass_names num), u, rule,
                     map (swap o `(resolve_spass_num NONE spass_names)) deps))