# HG changeset patch
# User blanchet
# Date 1304583374 -7200
# Node ID 3c2baf9b3c61d7250e79dda7bdb1f9e502779d8d
# Parent  60359df11dc484849591ad6990894134a94ac533
reverted 6efda6167e5d because unsound -- Vampire found a counterexample

diff -r 60359df11dc4 -r 3c2baf9b3c61 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 09:43:39 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 10:16:14 2011 +0200
@@ -618,10 +618,10 @@
 fun explicit_app arg head =
   let
     val head_T = combtyp_of head
-    val (_, res_T) = dest_funT head_T
+    val (arg_T, res_T) = dest_funT head_T
     val explicit_app =
       CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
-                 [res_T])
+                 [arg_T, res_T])
   in list_app explicit_app [head, arg] end
 fun list_explicit_app head args = fold explicit_app args head