proper firstorderization in Sledgehammer
authordesharna
Mon, 20 Sep 2021 10:22:59 +0200
changeset 74322 102b55e81aca
parent 74321 714e87ce6e9d
child 74326 b8a191ce08aa
child 74328 404ce20efc4c
proper firstorderization in Sledgehammer
src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Sep 19 21:55:11 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Sep 20 10:22:59 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 =