# HG changeset patch
# User blanchet
# Date 1330079012 -3600
# Node ID d0ef1d1562d77e09b1702aad9cad2373ccc05c78
# Parent  fc315796794ea35649b3b32f32bfcb461014daf2
fixed arity bug with "If" helpers for "If" that returns a function

diff -r fc315796794e -r d0ef1d1562d7 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Feb 24 09:40:02 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Feb 24 11:23:32 2012 +0100
@@ -1464,6 +1464,16 @@
                   | 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
@@ -1545,8 +1555,8 @@
           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)