make sure that "file" annotations are read correctly in SInE-E and E proofs
authorblanchet
Mon, 02 May 2011 14:21:57 +0200
changeset 42610 def5846169ce
parent 42609 b5e94b70bc06
child 42611 ec29be07cd9d
make sure that "file" annotations are read correctly in SInE-E and E proofs
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 =