1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 09:43:39 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 10:16:14 2011 +0200
     1.3 @@ -618,10 +618,10 @@
     1.4  fun explicit_app arg head =
     1.5    let
     1.6      val head_T = combtyp_of head
     1.7 -    val (_, res_T) = dest_funT head_T
     1.8 +    val (arg_T, res_T) = dest_funT head_T
     1.9      val explicit_app =
    1.10        CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
    1.11 -                 [res_T])
    1.12 +                 [arg_T, res_T])
    1.13    in list_app explicit_app [head, arg] end
    1.14  fun list_explicit_app head args = fold explicit_app args head
    1.15