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

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 15 16:20:23 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 15 16:42:09 2010 +0200
     2.3 @@ -173,7 +173,7 @@
     2.4                  (skolem_somes, @{const_name undefined})
     2.5                else case AList.find (op aconv) skolem_somes t of
     2.6                  s :: _ => (skolem_somes, s)
     2.7 -              | _ =>
     2.8 +              | [] =>
     2.9                  let
    2.10                    val s = skolem_theory_name ^ "." ^
    2.11                            skolem_name i (length skolem_somes)