diff -r 9a8acc5adfa3 -r 31babd4b1552 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -307,15 +307,21 @@
       >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x
 and parse_formula x =
   (parse_literal
-   -- Scan.option ((Scan.this_string tptp_implies >> K AImplies
-                    || Scan.this_string tptp_iff >> K AIff
-                    || Scan.this_string tptp_not_iff >> K ANotIff
-                    || Scan.this_string tptp_if >> K AIf
-                    || $$ tptp_or >> K AOr
-                    || $$ tptp_and >> K AAnd)
-                   -- parse_formula)
+   -- Scan.option ((Scan.this_string tptp_implies
+                    || Scan.this_string tptp_iff
+                    || Scan.this_string tptp_not_iff
+                    || Scan.this_string tptp_if
+                    || $$ tptp_or
+                    || $$ tptp_and) -- parse_formula)
    >> (fn (phi1, NONE) => phi1
-        | (phi1, SOME (c, phi2)) => mk_aconn c phi1 phi2)) x
+        | (phi1, SOME (c, phi2)) =>
+          if c = tptp_implies then mk_aconn AImplies phi1 phi2
+          else if c = tptp_iff then mk_aconn AIff phi1 phi2
+          else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2)
+          else if c = tptp_if then mk_aconn AImplies phi2 phi1
+          else if c = tptp_or then mk_aconn AOr phi1 phi2
+          else if c = tptp_and then mk_aconn AAnd phi1 phi2
+          else raise Fail ("impossible connective " ^ quote c))) x
 and parse_quantified_formula x =
   (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists)
    --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal