this looks like the most appropriate place to do the beta-eta-contraction

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Jun 23 09:40:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Jun 23 10:20:33 2010 +0200
@@ -140,6 +140,10 @@
     Const (@{const_name skolem_id}, T --> T) $ t
   end
 
+fun quasi_beta_eta_contract (Abs (s, T, t')) =
+    Abs (s, T, quasi_beta_eta_contract t')
+  | quasi_beta_eta_contract t = Envir.beta_eta_contract t
+
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun assume_skolem_funs inline s th =
   let
@@ -156,7 +160,8 @@
           (* Forms a lambda-abstraction over the formal parameters *)
           val rhs =
             list_abs_free (map dest_Free args,
-                           HOLogic.choice_const T $ body)
+                           HOLogic.choice_const T
+                           $ quasi_beta_eta_contract body)
             |> inline ? mk_skolem_id
           val def = Logic.mk_equals (c, rhs)
           val comb = list_comb (if inline then rhs else c, args)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Jun 23 09:40:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Jun 23 10:20:33 2010 +0200
@@ -166,7 +166,6 @@
       fun aux skolem_somes
               (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
           let
-            val t = Envir.beta_eta_contract t
             val (skolem_somes, s) =
               if i = ~1 then
                 (skolem_somes, @{const_name undefined})