# HG changeset patch
# User desharna
# Date 1632926947 -7200
# Node ID 162e63564e5aa7b208d9a417e01f3b0b50d8ef55
# Parent  776b74a9944930b2295f5392bfccf1d4dae69560# Parent  b9331caf92c3346d42802028c70aa155cdebca9b
merged

diff -r b9331caf92c3 -r 162e63564e5a src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 29 11:55:09 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 29 16:49:07 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)