1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Feb 10 17:10:47 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Feb 10 17:10:49 2012 +0100
     1.3 @@ -451,7 +451,7 @@
     1.4      -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
     1.5      -- parse_horn_clause --| $$ "."
     1.6      -- Scan.option (Scan.this_string "derived from formulae "
     1.7 -                    |-- Scan.repeat scan_general_id)
     1.8 +                    |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
     1.9    >> (fn ((((num, rule), deps), u), names) =>
    1.10           Inference ((num, resolve_spass_num names spass_names num), u, rule,
    1.11                      map (swap o `(resolve_spass_num NONE spass_names)) deps))