author | wenzelm |
Mon, 20 Sep 2021 15:11:13 +0200 | |
changeset 74326 | b8a191ce08aa |
parent 74322 | 102b55e81aca (diff) |
parent 74325 | 8d0c2d74ad63 (current diff) |
child 74327 | 9dca3df78b6a |
--- 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 =