# HG changeset patch
# User blanchet
# Date 1323900483 -3600
# Node ID 3be79bdcc70293a57315ca2407eb35e01b8c092f
# Parent  061ef175f7a1add1ad4efcf2ecfe4dce4cbe1166
fixed parsing of TPTP atoms

diff -r 061ef175f7a1 -r 3be79bdcc702 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 14 22:10:04 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 14 23:08:03 2011 +0100
@@ -267,7 +267,7 @@
 fun list_app (f, args) =
   fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f
 
-(* We ignore TFF and THF types for now. *)
+(* We currently ignore TFF and THF types. *)
 fun parse_type_stuff x =
   Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x
 and parse_arg x =
@@ -275,28 +275,17 @@
    || scan_general_id --| parse_type_stuff
         -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
       >> ATerm) x
-and parse_app x =
+and parse_term x =
   (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x
-and parse_term x =
-  (parse_app -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal
-                             -- parse_app)
-   >> (fn (u1, NONE) => u1
-        | (u1, SOME (NONE, u2)) => ATerm ("equal", [u1, u2])
-        | (u1, SOME (SOME _, u2)) =>
-          ATerm (tptp_not, [ATerm ("equal", [u1, u2])]))) x
 and parse_terms x =
   (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
 
-(* TODO: Avoid duplication with "parse_term" above. *)
 fun parse_atom x =
   (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal
                               -- parse_term)
    >> (fn (u1, NONE) => AAtom u1
-        | (u1, SOME (NONE, u2)) => AAtom (ATerm ("equal", [u1, u2]))
-        | (u1, SOME (SOME _, u2)) =>
-          mk_anot (AAtom (ATerm ("equal", [u1, u2]))))) x
-
-fun ho_term_head (ATerm (s, _)) = s
+        | (u1, SOME (neg, u2)) =>
+          AAtom (ATerm ("equal", [u1, u2])) |> is_some neg ? mk_anot)) x
 
 (* TPTP formulas are fully parenthesized, so we don't need to worry about
    operator precedence. *)
@@ -328,7 +317,7 @@
    --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
    >> (fn ((q, ts), phi) =>
           (* We ignore TFF and THF types for now. *)
-          AQuant (q, map (rpair NONE o ho_term_head) ts, phi))) x
+          AQuant (q, map (fn ATerm (s, _) => (s, NONE)) ts, phi))) x
 
 val parse_tstp_extra_arguments =
   Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))