src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML

 signature SLEDGEHAMMER_FACT_PREPROCESSOR =
 sig
   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
   val type_has_topsort: typ -> bool
   val cnf_rules_pairs:

 val chained_prefix = "Sledgehammer.chained_"
 
 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 = "$"
 
 fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
 

 exception Clausify_failure of theory;
 
 
 (**** 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);
 
 fun skolem_name thm_name j var_name =
   skolem_prefix ^ thm_name ^ "_" ^ Int.toString j ^

         (*Existential: declare a Skolem function, then insert into body and continue*)
         let
           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
           val cdef = id ^ "_def"
           val ((_, ax), thy) =

       | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
       | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
       | 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
     val skolem_count = Unsynchronized.ref 0   (* FIXME ??? *)
     fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) defs =

           val args = subtract (op =) skos (OldTerm.term_frees body) (*the formal parameters*)
           val Ts = map type_of args
           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)
         in dec_sko (subst_bound (comb, p)) (def :: defs) end
       | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =

 (*Given the definition of a Skolem function, return a theorem to replace
   an existential formula by a use of that function.
    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.*)
        |> Thm.varifyT_global
   end;

     []
   else
     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
       cnfs |> map introduce_combinators
            |> Variable.export ctxt ctxt0

     val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
       if member (op =) multi_base_blacklist (Long_Name.base_name name) then
         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)
   in
     if null new_facts then