avoid "Empty" exception by making sure that a certain optimization only is attempted when it makes sense

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:18 2011 +0200
@@ -682,6 +682,7 @@
                anyway, by distinguishing overloads only on the homogenized
                result type. *)
             if s = const_prefix ^ explicit_app_base andalso
+               length T_args = 2 andalso
                not (is_type_sys_virtually_sound type_sys) then
               T_args |> map (homogenized_type ctxt nonmono_Ts level)
                      |> (fn Ts => let val T = hd Ts --> nth Ts 1 in