# HG changeset patch
# User wenzelm
# Date 1632949440 -7200
# Node ID a480ac43f51a703847897f6c0efa2efedca78bc2
# Parent  162e63564e5aa7b208d9a417e01f3b0b50d8ef55# Parent  e80c4cde606476ac666ede7749ce2d9213530639
merged

diff -r e80c4cde6064 -r a480ac43f51a src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 29 22:54:38 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Sep 29 23:04:00 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)