src/HOL/Tools/ATP/atp_problem_generate.ML

                                     sym_tab
                     end
                   | NONE =>
                     let
                       val pred_sym = top_level andalso not bool_vars
+                      val ary =
+                        case unprefix_and_unascii const_prefix s of
+                          SOME s =>
+                          if not (String.isSubstring uncurried_alias_sep s)
+                             andalso (s |> unmangled_const_name |> hd
+                                        |> invert_const) = @{const_name If} then
+                            Integer.min ary 3
+                          else
+                            ary
+                        | NONE => ary
                       val min_ary =
                         case app_op_level of
                           Incomplete_Apply => ary
                         | Sufficient_Apply =>
                           fold (consider_var_ary T) fun_var_Ts ary

         case head of
           IConst (name as (s, _), T, T_args) =>
           if uncurried_aliases andalso String.isPrefix const_prefix s then
             let
               val ary = length args
-              val name = name |> ary > min_ary_of sym_tab s
-                                 ? aliased_uncurried ary
+              val name =
+                name |> ary > min_ary_of sym_tab s ? aliased_uncurried ary
             in list_app (IConst (name, T, T_args)) args end
           else
             args |> chop (min_ary_of sym_tab s)
                  |>> list_app head |-> list_app_ops
         | _ => list_app_ops head args