# HG changeset patch
# User blanchet
# Date 1304338917 -7200
# Node ID def5846169ce2ecdfc4906a7d94ef3a6db3a481e
# Parent  b5e94b70bc06fe89a968bd8607e41e389f9e531c
make sure that "file" annotations are read correctly in SInE-E and E proofs

diff -r b5e94b70bc06 -r def5846169ce src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 02 14:10:09 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 02 14:21:57 2011 +0200
@@ -251,9 +251,8 @@
 
 (* Generalized first-order terms, which include file names, numbers, etc. *)
 fun parse_annotation x =
-  ((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id)
-      >> filter (is_some o Int.fromString))
-   -- Scan.optional parse_annotation [] >> op @
+  ((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id))
+     -- Scan.optional parse_annotation [] >> op @
    || $$ "(" |-- parse_annotations --| $$ ")"
    || $$ "[" |-- parse_annotations --| $$ "]") x
 and parse_annotations x =