# 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;