# HG changeset patch
# User blanchet
# Date 1305206958 -7200
# Node ID 70fc448a18153898c1f6dc5f2fad824a6815915c
# Parent  64dea91bbe0eb72d6dd637a5ecad4b9510273aae
avoid "Empty" exception by making sure that a certain optimization only is attempted when it makes sense

diff -r 64dea91bbe0e -r 70fc448a1815 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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