# HG changeset patch
# User blanchet
# Date 1626698873 -7200
# Node ID d0b190b4f15dce58d58c991dd8bf003ff8c11508
# Parent  a0c9fc9c7dbeda95ceba91c61b02d8c74b3834e5
parse TPTP operator @ also when not parenthesized

diff -r a0c9fc9c7dbe -r d0b190b4f15d src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 19 14:47:52 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jul 19 14:47:53 2021 +0200
@@ -150,10 +150,6 @@
   else
     ""
 
-val missing_message_tail =
-  " appears to be missing; you will need to install it if you want to invoke \
-  \remote provers"
-
 fun from_lemmas [] = ""
   | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
 
@@ -497,15 +493,15 @@
   else if q = tptp_hilbert_the then tptp_hilbert_the
   else raise Fail ("unrecognized quantification: " ^ q)
 
-fun remove_hol_app (ATerm ((x, ty), arg)) =
-    if x = tptp_app then
+fun remove_hol_app (ATerm ((s, ty), arg)) =
+    if s = tptp_app then
       (case arg of
-        ATerm ((x, ty), arg) :: t => remove_hol_app (ATerm ((x, ty), map remove_hol_app arg @ t))
+        ATerm ((s, ty), arg) :: t => remove_hol_app (ATerm ((s, ty), map remove_hol_app arg @ t))
       | [AAbs ((var, tvar), phi), t] =>
         remove_hol_app (AAbs ((var, tvar), map remove_hol_app phi @ [t])))
     else
-      ATerm ((x, ty), map remove_hol_app arg)
-  | remove_hol_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_hol_app arg), t)
+      ATerm ((s, ty), map remove_hol_app arg)
+  | remove_hol_app (AAbs (((s, ty), arg), t)) = AAbs (((s, ty), remove_hol_app arg), t)
 
 fun parse_hol_typed_var x =
   (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)
@@ -530,10 +526,11 @@
   || $$ "(" |-- parse_hol_term --| $$ ")"
   || parse_binary_op >> mk_simple_aterm) x
 and parse_hol_term x =
-  (parse_simple_hol_term -- Scan.option (parse_binary_op -- parse_hol_term)
-    >> (fn (t1, SOME (c, t2)) =>
-           if c = tptp_app then mk_app t1 t2 else mk_apps (mk_simple_aterm c) [t1, t2]
-         | (t, NONE) => t)) x
+  (parse_simple_hol_term -- Scan.repeat (parse_binary_op -- parse_simple_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
 
 fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x