diff -r a7538ad74997 -r 6467c99c4872 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 01 14:53:46 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 01 17:15:06 2012 +0100
@@ -439,10 +439,15 @@
                 []
   | NONE => []
 
+val parse_spass_debug =
+  Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ","))
+               --| $$ ")")
+
 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. *)
 fun parse_spass_line spass_names =
-  scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" -- Symbol.scan_id
-    -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
+  parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
+    -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
+    -- parse_horn_clause --| $$ "."
   >> (fn (((num, rule), deps), u) =>
          Inference ((num, resolve_spass_num spass_names num), u, rule,
                     map (swap o `(resolve_spass_num spass_names)) deps))