fixed me -- indeed this was wrong, as demonstrated by the predicate-free HO output (e.g. ehoh with keep_lams)

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jan 23 03:29:34 2019 +0000
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jan 23 17:20:35 2019 +0100
@@ -1979,8 +1979,8 @@
             map (term Elsewhere) args |> mk_aterm type_enc name []
           | IAbs ((name, T), tm) =>
             if is_type_enc_higher_order type_enc then
-              AAbs (((name, native_atp_type_of_typ type_enc true 0 T), (* FIXME? why "true"? *)
-                     term Elsewhere tm), map (term Elsewhere) args)
+              AAbs (((name, native_atp_type_of_typ type_enc false 0 T), term Elsewhere tm),
+                map (term Elsewhere) args)
             else
               raise Fail "unexpected lambda-abstraction"
           | IApp _ => raise Fail "impossible \"IApp\"")