diff -r 6c9f23863808 -r 2bf7e6136047 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Jun 12 15:48:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Mon Jun 14 10:36:01 2010 +0200
@@ -10,11 +10,10 @@
   val chained_prefix: string
   val trace: bool Unsynchronized.ref
   val trace_msg: (unit -> string) -> unit
-  val skolem_Eps_pseudo_theory: string
+  val skolem_theory_name: string
   val skolem_prefix: string
   val skolem_infix: string
   val is_skolem_const_name: string -> bool
-  val skolem_type_and_args: typ -> term -> typ * term list
   val cnf_axiom: theory -> thm -> thm list
   val multi_base_blacklist: string list
   val is_theorem_bad_for_atps: thm -> bool
@@ -42,7 +41,7 @@
 val trace = Unsynchronized.ref false;
 fun trace_msg msg = if !trace then tracing (msg ()) else ();
 
-val skolem_Eps_pseudo_theory = "Sledgehammer.Eps"
+val skolem_theory_name = "Sledgehammer.Sko"
 val skolem_prefix = "sko_"
 val skolem_infix = "$"
 
@@ -76,9 +75,6 @@
 
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
 
-fun skolem_Eps_const T =
-  Const (@{const_name skolem_Eps}, (T --> HOLogic.boolT) --> T)
-
 (*Keep the full complexity of the original name*)
 fun flatten_name s = space_implode "_X" (Long_Name.explode s);
 
@@ -120,7 +116,7 @@
           val id = skolem_name s (Unsynchronized.inc skolem_count) s'
           val (cT, args) = skolem_type_and_args T body
           val rhs = list_abs_free (map dest_Free args,
-                                   skolem_Eps_const T $ body)
+                                   HOLogic.choice_const T $ body)
                   (*Forms a lambda-abstraction over the formal parameters*)
           val (c, thy) =
             Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
@@ -139,6 +135,9 @@
       | dec_sko t thx = thx
   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
+
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun assume_skolem_funs inline s th =
   let
@@ -152,7 +151,9 @@
           val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
           val id = skolem_name s (Unsynchronized.inc skolem_count) s'
           val c = Free (id, cT)
-          val rhs = list_abs_free (map dest_Free args, skolem_Eps_const T $ body)
+          val rhs = list_abs_free (map dest_Free args,
+                                   HOLogic.choice_const T $ body)
+                    |> inline ? mk_skolem_id
                 (*Forms a lambda-abstraction over the formal parameters*)
           val def = Logic.mk_equals (c, rhs)
           val comb = list_comb (if inline then rhs else c, args)
@@ -295,23 +296,26 @@
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
 fun skolem_theorem_of_def inline def =
   let
-      val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
-      val (ch, frees) = c_variant_abs_multi (rhs, [])
-      val (chilbert,cabs) = Thm.dest_comb ch
+      val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
+      val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
+      val (ch, frees) = c_variant_abs_multi (rhs', [])
+      val (chilbert, cabs) = ch |> Thm.dest_comb
       val thy = Thm.theory_of_cterm chilbert
       val t = Thm.term_of chilbert
       val T =
         case t of
-          Const (@{const_name skolem_Eps}, Type (@{type_name fun}, [_, T])) => T
-        | _ => raise THM ("skolem_theorem_of_def: expected \"Eps\"", 0, [def])
+          Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
+        | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
       val cex = Thm.cterm_of thy (HOLogic.exists_const T)
       val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
       and conc =
         Drule.list_comb (if inline then rhs else c, frees)
         |> Drule.beta_conv cabs |> c_mkTrueprop
       fun tacf [prem] =
-        (if inline then all_tac else rewrite_goals_tac [def])
-        THEN rtac (prem RS @{thm skolem_someI_ex}) 1
+        (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
+         else rewrite_goals_tac [def])
+        THEN rtac ((prem |> inline ? rewrite_rule @{thms skolem_id_def_raw})
+                   RS @{thm someI_ex}) 1
   in  Goal.prove_internal [ex_tm] conc tacf
        |> forall_intr_list frees
        |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
@@ -398,12 +402,7 @@
     let
       val ctxt0 = Variable.global_thm_context th
       val (nnfth, ctxt) = to_nnf th ctxt0
-
-      val inline = false
-(*
-FIXME: Reintroduce code:
       val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
-*)
       val defs = skolem_theorems_of_assume inline s nnfth
       val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
     in
@@ -492,7 +491,8 @@
         I
       else
         fold_index (fn (i, th) =>
-          if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
+          if is_theorem_bad_for_atps th orelse
+             is_some (lookup_cache thy th) then
             I
           else
             cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)