# HG changeset patch
# User wenzelm
# Date 1632143473 -7200
# Node ID b8a191ce08aabb6f0bb652aff4bd084e7897cac9
# Parent  102b55e81aca9b7ed33a9b23d8a50d598d18bf98# Parent  8d0c2d74ad63586edeea90317da85c6e188f81c5
merged

diff -r 8d0c2d74ad63 -r b8a191ce08aa src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Sep 20 13:52:09 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Sep 20 15:11:13 2021 +0200
@@ -1738,6 +1738,8 @@
           in
             args |> chop ary |>> list_app head |> list_app_ops
           end
+        | IAbs ((name, T), tm) =>
+          list_app_ops (IAbs ((name, T), introduce_app_ops tm), args)
         | _ => list_app_ops (head, args))
       end
     fun introduce_predicators tm =