# HG changeset patch
# User blanchet
# Date 1361377888 -3600
# Node ID e5ef7a18f4a3c88bbbec158d5203dc703e3e831a
# Parent  ec16ec9ab8d53e375fd334708ea9cc79a549f001
generalize syntax of SPASS proofs

diff -r ec16ec9ab8d5 -r e5ef7a18f4a3 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 20 17:15:06 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Feb 20 17:31:28 2013 +0100
@@ -460,8 +460,9 @@
 (* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
            derived from formulae <ident>* *)
 fun parse_spass_line x =
-  (parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
-     -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]"
+  (parse_spass_debug |-- scan_general_id --| $$ "[" --|
+     Scan.many1 Symbol.is_digit --| $$ ":" -- Symbol.scan_ascii_id
+     -- parse_spass_annotations --| $$ "]"
      -- parse_horn_clause --| $$ "."
      -- Scan.option (Scan.this_string "derived from formulae "
                      |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))