Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
authorwenzelm
Thu, 05 Jul 2007 20:01:29 +0200
changeset 23592 ba0912262b2c
parent 23591 d32a85385e17
child 23593 fd12f7d56bd7
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac; simplified ObjectLogic.atomize;
src/HOL/Tools/res_axioms.ML file | annotate | diff | comparison | revisions 
--- 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.*)
isabelle