1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:56:06 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:56:06 2011 +0200
     1.3 @@ -1059,8 +1059,7 @@
     1.4            val bool_vars' = bool_vars orelse body_type T = @{typ bool}
     1.5            fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
     1.6              {pred_sym = pred_sym andalso not bool_vars',
     1.7 -             min_ary =
     1.8 -               fold (fn T' => consider_var_arity T' T) types min_ary,
     1.9 +             min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
    1.10               max_ary = max_ary, types = types}
    1.11            val fun_var_Ts' =
    1.12              fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
    1.13 @@ -1069,8 +1068,7 @@
    1.14               pointer_eq (fun_var_Ts', fun_var_Ts) then
    1.15              accum
    1.16            else
    1.17 -            ((bool_vars', fun_var_Ts'),
    1.18 -             Symtab.map (K repair_min_arity) sym_tab)
    1.19 +            ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
    1.20          end
    1.21        else
    1.22          accum
    1.23 @@ -1833,7 +1831,7 @@
    1.24        repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
    1.25                         |> map repair
    1.26      val lavish_nonmono_Ts =
    1.27 -      if null nonmono_Ts orelse
    1.28 +      if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
    1.29           polymorphism_of_type_sys type_sys <> Polymorphic then
    1.30          nonmono_Ts
    1.31        else