# HG changeset patch
# User blanchet
# Date 1276612929 -7200
# Node ID 2d76997730a60e626c4e5c08393287e31a08988e
# Parent  ed79fa6200124708e4b1dc33e4e75417d25fc4ba
found missing beta-eta-contraction

diff -r ed79fa620012 -r 2d76997730a6 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- 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
diff -r ed79fa620012 -r 2d76997730a6 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 15 16:20:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 15 16:42:09 2010 +0200
@@ -173,7 +173,7 @@
                 (skolem_somes, @{const_name undefined})
               else case AList.find (op aconv) skolem_somes t of
                 s :: _ => (skolem_somes, s)
-              | _ =>
+              | [] =>
                 let
                   val s = skolem_theory_name ^ "." ^
                           skolem_name i (length skolem_somes)