src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 12:19:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 13:17:17 2010 +0200
@@ -168,6 +168,7 @@
       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})