# HG changeset patch
# User blanchet
# Date 1308141401 -7200
# Node ID 5b499c360df6bdaabb4855bf98deef951f6d09db
# Parent  8d3a5b7b9a001c82eacaa1c1b166b90091b18829
type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases

diff -r 8d3a5b7b9a00 -r 5b499c360df6 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 10 17:52:09 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 15 14:36:41 2011 +0200
@@ -1699,8 +1699,6 @@
           |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
   end
 
-fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
-
 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
         type_sys n s j (s', T_args, T, _, ary, in_conj) =
   let
@@ -1708,13 +1706,14 @@
       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
       else (Axiom, I)
     val (arg_Ts, res_T) = chop_fun ary T
+    val num_args = length arg_Ts
     val bound_names =
-      1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
+      1 upto num_args |> map (`I o make_bound_var o string_of_int)
     val bounds =
       bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
     val bound_Ts =
-      arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
-                             else NONE)
+      if n > 1 andalso should_drop_arg_type_args type_sys then map SOME arg_Ts
+      else replicate num_args NONE
   in
     Formula (preds_sym_formula_prefix ^ s ^
              (if n > 1 then "_" ^ string_of_int j else ""), kind,