diff -r 26afa11a1fb2 -r ff72d3ddc898 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- 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})