# HG changeset patch
# User desharna
# Date 1632842061 -7200
# Node ID 776b74a9944930b2295f5392bfccf1d4dae69560
# Parent  23db3493478fb1cb429a808c1e2179417e60d263
tuned TPTP parsing of THF function application

diff -r 23db3493478f -r 776b74a99449 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 29 09:58:19 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Sep 28 17:14:21 2021 +0200
@@ -496,15 +496,15 @@
   else if q = tptp_hilbert_the then tptp_hilbert_the
   else raise Fail ("unrecognized quantification: " ^ q)
 
-fun remove_hol_app (ATerm ((s, ty), arg)) =
+fun remove_hol_app (ATerm ((s, ty), args)) =
     if s = tptp_app then
-      (case arg of
-        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])))
+      (case args of
+        ATerm (f, xs) :: ys => remove_hol_app (ATerm (f, xs @ ys))
+      | AAbs ((var, phi), xs) :: ys => remove_hol_app (AAbs ((var, phi), xs @ ys)))
     else
-      ATerm ((s, ty), map remove_hol_app arg)
-  | remove_hol_app (AAbs (((s, ty), arg), t)) = AAbs (((s, ty), remove_hol_app arg), t)
+      ATerm ((s, ty), map remove_hol_app args)
+  | remove_hol_app (AAbs ((var, phi), args)) =
+    AAbs ((var, remove_hol_app phi), map remove_hol_app args)
 
 fun parse_hol_typed_var x =
   (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type)