# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID 3031d342d5148d9ac97686f9129f3a9e30899de5
# Parent  b9754f26c7bcbfa8c0d647427b61b2127ac30bd7
fixed parsing of not in ATP proofs (e.g. ~x | y is (~x) | y, not ~(x | y))

diff -r b9754f26c7bc -r 3031d342d514 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:24 2011 +0200
@@ -262,7 +262,7 @@
        >> (fn ((q, ts), phi) =>
               (* FIXME: TFF *)
               AQuant (q, map (rpair NONE o fo_term_head) ts, phi))
-    || $$ "~" |-- parse_formula >> mk_anot
+    || $$ "~" |-- ($$ "(" |-- parse_formula --| $$ ")" || parse_atom) >> mk_anot
     || parse_atom)
    -- Scan.option ((Scan.this_string "=>" >> K AImplies
                     || Scan.this_string "<=>" >> K AIff