--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jul 20 00:37:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jul 20 00:37:42 2011 +0200
@@ -1733,7 +1733,7 @@
1 upto num_args |> map (`I o make_bound_var o string_of_int)
val bounds =
bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
- val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
+ val sym_needs_arg_types = exists (curry (op =) dummyT) T_args)
fun should_keep_arg_type T =
sym_needs_arg_types orelse
not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)