# HG changeset patch
# User blanchet
# Date 1643714083 -3600
# Node ID 632c9ae415fac32f5a3d7c2b5a7297c814907f66
# Parent  8ce2469920bf7d5533def478e6e079755b22fe4a
adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs

diff -r 8ce2469920bf -r 632c9ae415fa src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Feb 01 11:52:40 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Feb 01 12:14:43 2022 +0100
@@ -477,7 +477,7 @@
 
 val tptp_binary_ops =
   [tptp_and, tptp_or, tptp_implies, tptp_iff, tptp_if, tptp_equal, tptp_not_equal, tptp_not_and,
-   tptp_not_or, tptp_not_iff, tptp_app]
+   tptp_not_or, tptp_not_iff]
 
 fun parse_one_in_list xs =
   foldl1 (op ||) (map Scan.this_string xs)
@@ -531,12 +531,13 @@
   || parse_hol_quantifier >> mk_simple_aterm
   || $$ "(" |-- parse_hol_term --| $$ ")"
   || parse_binary_op >> mk_simple_aterm) x
+and parse_applied_hol_term x =
+  (parse_simple_hol_term -- Scan.repeat (Scan.this_string tptp_app |-- parse_simple_hol_term)
+    >> (fn (t1, tis) => fold (fn ti => fn left => mk_app left ti) tis t1)) x
 and parse_hol_term x =
-  (parse_simple_hol_term -- Scan.repeat (parse_binary_op -- parse_simple_hol_term)
+  (parse_applied_hol_term -- Scan.repeat (parse_binary_op -- parse_applied_hol_term)
     >> (fn (t1, c_ti_s) =>
-        fold (fn (c, ti) => fn left =>
-            if c = tptp_app then mk_app left ti else mk_apps (mk_simple_aterm c) [left, ti])
-          c_ti_s t1)) x
+          fold (fn (c, ti) => fn left => mk_apps (mk_simple_aterm c) [left, ti]) c_ti_s t1)) x
 
 fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x