1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 20 17:15:06 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 20 17:31:28 2013 +0100
     1.3 @@ -460,8 +460,9 @@
     1.4  (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
     1.5             derived from formulae <ident>* *)
     1.6  fun parse_spass_line x =
     1.7 -  (parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
     1.8 -     -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]"
     1.9 +  (parse_spass_debug |-- scan_general_id --| $$ "[" --|
    1.10 +     Scan.many1 Symbol.is_digit --| $$ ":" -- Symbol.scan_ascii_id
    1.11 +     -- parse_spass_annotations --| $$ "]"
    1.12       -- parse_horn_clause --| $$ "."
    1.13       -- Scan.option (Scan.this_string "derived from formulae "
    1.14                       |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))