# HG changeset patch
# User blanchet
# Date 1352197256 -3600
# Node ID f046cf7be176f44dd1544b9384bb5aafeadef860
# Parent  17488e45eb5acb7f6c1cfe425aa2b2342aee5a95
correct parsing of E dependencies

diff -r 17488e45eb5a -r f046cf7be176 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 06 11:20:56 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 06 11:20:56 2012 +0100
@@ -250,18 +250,22 @@
 
 (* "skip_term" is there to cope with Waldmeister nonsense such as
    "theory(equality)". *)
-val parse_dependency = scan_general_id --| skip_term
-val parse_dependencies =
-  parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency)
-
-fun parse_source x =
-  (Scan.this_string "file" |-- $$ "(" |-- scan_general_id --
-     Scan.option ($$ "," |-- scan_general_id) --| $$ ")"
-     >> File_Source
-   || Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
-        --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
-        -- parse_dependencies --| $$ "]" --| $$ ")"
-       >> Inference_Source
+fun parse_dependency x =
+  (parse_inference_source >> snd
+   || scan_general_id --| skip_term >> single) x
+and parse_dependencies x =
+  (parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency)
+   >> flat) x
+and parse_file_source x =
+  (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
+   -- Scan.option ($$ "," |-- scan_general_id) --| $$ ")") x
+and parse_inference_source x =
+  (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
+   --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
+   -- parse_dependencies --| $$ "]" --| $$ ")") x
+and parse_source x =
+  (parse_file_source >> File_Source
+   || parse_inference_source >> Inference_Source
    || skip_term >> K dummy_inference) x
 
 fun list_app (f, args) =