# HG changeset patch
# User blanchet
# Date 1311115062 -7200
# Node ID 14d34bd434b8cdba93cdd4f6bd8a4fdfb65203c8
# Parent  1ace987e22e576e48c014abe28affe2ac42e38f4
generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart

diff -r 1ace987e22e5 -r 14d34bd434b8 src/HOL/Tools/ATP/atp_translate.ML
--- 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)