--- 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)