--- a/src/HOL/Tools/res_axioms.ML Thu Jul 05 20:01:28 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Thu Jul 05 20:01:29 2007 +0200
@@ -416,7 +416,7 @@
fun to_nnf th =
th |> transfer_to_ATP_Linkup
|> transform_elim |> zero_var_indexes |> freeze_thm
- |> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
+ |> Conv.fconv_rule ObjectLogic.atomize |> make_nnf |> strip_lambdas ~1;
(*Generate Skolem functions for a theorem supplied in nnf*)
fun skolem_of_nnf s th =
@@ -640,7 +640,7 @@
(*** Converting a subgoal into negated conjecture clauses. ***)
-val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac];
+val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, skolemize_tac];
(*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
it can introduce TVars, which are useless in conjecture clauses.*)