# HG changeset patch
# User blanchet
# Date 1368033403 -7200
# Node ID bbbacaef19a6b0b19191bf4b5000068a59d2f2c2
# Parent  16f3b9d4e515adc472afbbb31d82e407408cda74
avoid polymorphic uncurried aliases with more arguments than there are arguments in the most general type of a HOL constant, to dodge issues at declaration time

diff -r 16f3b9d4e515 -r bbbacaef19a6 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 08 16:38:02 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 08 19:16:43 2013 +0200
@@ -1177,7 +1177,8 @@
       if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
       else T_args
     | SOME s'' =>
-      filter_type_args thy constrs type_enc (unmangled_invert_const s'') ary T_args
+      filter_type_args thy constrs type_enc (unmangled_invert_const s'') ary
+                       T_args
 fun filter_type_args_in_iterm thy constrs type_enc =
   let
     fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
@@ -1644,21 +1645,42 @@
                        completish =
   let
     fun do_app arg head = mk_app_op type_enc head arg
-    fun list_app_ops head args = fold do_app args head
+    fun list_app_ops (head, args) = fold do_app args head
     fun introduce_app_ops tm =
       let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
         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
-            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
+          let
+            val min_ary = min_ary_of sym_tab s
+            val ary =
+              if uncurried_aliases andalso String.isPrefix const_prefix s then
+                let
+                  val ary = length args
+                  (* In polymorphic native type encodings, it is impossible to
+                     declare a fully polymorphic symbol that takes more arguments
+                     than its signature (even though such concrete instances, where
+                     a type variable is instantiated by a function type, are
+                     possible.) *)
+                  val official_ary =
+                    if is_type_enc_polymorphic type_enc then
+                      case unprefix_and_unascii const_prefix s of
+                        SOME s' =>
+                        (case try (robust_const_ary thy) (invert_const s') of
+                           SOME ary => ary
+                         | NONE => min_ary)
+                      | NONE => min_ary
+                    else
+                      1000000000 (* irrealistically big arity *)
+                in Int.min (ary, official_ary) end
+              else
+                min_ary
+            val head =
+              if ary = min_ary then head
+              else IConst (aliased_uncurried ary name, T, T_args)
+          in
+            args |> chop ary |>> list_app head |> list_app_ops
+          end
+        | _ => list_app_ops (head, args)
       end
     fun introduce_predicators tm =
       case strip_iterm_comb tm of