# HG changeset patch
# User wenzelm
# Date 1183658489 -7200
# Node ID ba0912262b2c79b8a1636151a90e1816da3d99d2
# Parent  d32a85385e177a418a7704874e5c42893ef8ee6c
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
simplified ObjectLogic.atomize;

diff -r d32a85385e17 -r ba0912262b2c src/HOL/Tools/res_axioms.ML
--- 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.*)