# HG changeset patch
# User blanchet
# Date 1277281233 -7200
# Node ID ff72d3ddc898f857c9e1043413949685946145c8
# Parent  26afa11a1fb20b5e73b95f3d76b5337df14557c5
this looks like the most appropriate place to do the beta-eta-contraction

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