src/HOL/Tools/res_axioms.ML

 
 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
 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 =
   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
 

   >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
 
 
 (*** 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.*)
 val no_tvars = null o term_tvars o prop_of;