--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 15 16:20:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 15 16:42:09 2010 +0200
@@ -136,7 +136,9 @@
in dec_sko (prop_of th) ([], thy) end
fun mk_skolem_id t =
- let val T = fastype_of t in Const (@{const_name skolem_id}, T --> T) $ t end
+ let val T = fastype_of t in
+ Const (@{const_name skolem_id}, T --> T) $ Envir.beta_eta_contract t
+ end
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skolem_funs inline s th =
@@ -407,7 +409,6 @@
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
- val inline = false (* FIXME: temporary *)
val defs = skolem_theorems_of_assume inline s nnfth
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
in