1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jun 10 17:52:09 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 15 14:36:41 2011 +0200
     1.3 @@ -1699,8 +1699,6 @@
     1.4            |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
     1.5    end
     1.6  
     1.7 -fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
     1.8 -
     1.9  fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
    1.10          type_sys n s j (s', T_args, T, _, ary, in_conj) =
    1.11    let
    1.12 @@ -1708,13 +1706,14 @@
    1.13        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
    1.14        else (Axiom, I)
    1.15      val (arg_Ts, res_T) = chop_fun ary T
    1.16 +    val num_args = length arg_Ts
    1.17      val bound_names =
    1.18 -      1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
    1.19 +      1 upto num_args |> map (`I o make_bound_var o string_of_int)
    1.20      val bounds =
    1.21        bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
    1.22      val bound_Ts =
    1.23 -      arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
    1.24 -                             else NONE)
    1.25 +      if n > 1 andalso should_drop_arg_type_args type_sys then map SOME arg_Ts
    1.26 +      else replicate num_args NONE
    1.27    in
    1.28      Formula (preds_sym_formula_prefix ^ s ^
    1.29               (if n > 1 then "_" ^ string_of_int j else ""), kind,