author | desharna |
Tue, 07 Dec 2021 23:27:06 +0100 | |
changeset 74900 | 21ea15129166 |
parent 74899 | b4beb55c574e |
child 74901 | 2cbb5f6a854f |
--- 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)