# HG changeset patch
# User desharna
# Date 1638916026 -3600
# Node ID 21ea1512916638275f6dd0c03cc25d02fa29cb4f
# Parent  b4beb55c574eac369ed3079677fdf98197dd22ca
fixed TPTP generation of multi-arity expressions

diff -r b4beb55c574e -r 21ea15129166 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Nov 29 15:45:17 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Dec 07 23:27:06 2021 +0100
@@ -1621,7 +1621,8 @@
     fun consider_var_ary const_T var_T max_ary =
       let
         fun iter ary T =
-          if ary = max_ary orelse type_instance thy var_T T orelse type_instance thy T var_T then
+          if ary = max_ary orelse type_instance thy var_T T orelse type_instance thy T var_T orelse
+             not (can dest_funT T) then
             ary
           else
             iter (ary + 1) (range_type T)