src/HOL/Tools/Sledgehammer/clausifier.ML

     fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) rhss =
         (*Existential: declare a Skolem function, then insert into body and continue*)
         let
           val args = OldTerm.term_frees body
           val Ts = map type_of args
-          val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
+          val cT = Ts ---> T
           (* Forms a lambda-abstraction over the formal parameters *)
           val rhs =
             list_abs_free (map dest_Free args,
                            HOLogic.choice_const T $ beta_eta_under_lambdas body)
             |> mk_skolem_id

 
 (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
 
 (*Returns the vars of a theorem*)
 fun vars_of_thm th =
-  map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
+  map (cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
 
 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
 (* Removes the lambdas from an equation of the form "t = (%x. u)".
    (Cf. "extensionalize_term" in "ATP_Systems".) *)

                      "\nException message: " ^ msg ^ ".");
             (* A type variable of sort "{}" will make abstraction fail. *)
             TrueI)
 
 (*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
+val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
 
 (*Given an abstraction over n variables, replace the bound variables by free
   ones. Return the body, along with the list of free variables.*)
 fun c_variant_abs_multi (ct0, vars) =
       let val (cv,ct) = Thm.dest_abs NONE ct0

 (* 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 thy rhs0 =
   let
-    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
+    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
     val rhs' = rhs |> Thm.dest_comb |> snd
     val (ch, frees) = c_variant_abs_multi (rhs', [])
     val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
     val T =
       case hilbert of
         Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
       | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
-    val cex = Thm.cterm_of thy (HOLogic.exists_const T)
+    val cex = cterm_of thy (HOLogic.exists_const T)
     val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
     val conc =
       Drule.list_comb (rhs, frees)
       |> Drule.beta_conv cabs |> Thm.capply cTrueprop
     fun tacf [prem] =