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
--- 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,