# HG changeset patch
# User blanchet
# Date 1281343137 -7200
# Node ID aee5862973e021670e2b834028e175ff6aa981d5
# Parent  2f340f254c9916f458f0a5dd3a8c953308cc8ffc
remove now needless "Thm.transfer"

diff -r 2f340f254c99 -r aee5862973e0 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 09 10:13:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 09 10:38:57 2010 +0200
@@ -82,7 +82,6 @@
 
 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
-(* ### FIXME: removes only one lambda? *)
 (* Removes the lambdas from an equation of the form "t = (%x. u)".
    (Cf. "extensionalize_term" in "ATP_Systems".) *)
 fun extensionalize_theorem th =
@@ -231,8 +230,8 @@
                     |> Meson.make_nnf ctxt
   in  (th3, ctxt)  end;
 
-(* Skolemize a named theorem, with Skolem functions as additional premises. *)
-fun skolemize_theorem thy th =
+(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
+fun cnf_axiom thy th =
   let
     val ctxt0 = Variable.global_thm_context th
     val (nnfth, ctxt) = to_nnf th ctxt0
@@ -247,8 +246,4 @@
   end
   handle THM _ => []
 
-(* Convert Isabelle theorems into axiom clauses. *)
-(* FIXME: is transfer necessary? *)
-fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
-
 end;