src/HOL/Tools/res_atp_setup.ML

--- a/src/HOL/Tools/res_atp_setup.ML	Fri Dec 23 15:21:05 2005 +0100
+++ b/src/HOL/Tools/res_atp_setup.ML	Fri Dec 23 17:34:46 2005 +0100
@@ -284,9 +284,8 @@
 
 fun cnf_hyps_thms ctxt = 
     let val ths = ProofContext.prems_of ctxt
-	val prems = ResClause.union_all (map ResAxioms.cnf_axiom_aux ths)
     in
-	prems
+	ResClause.union_all (map ResAxioms.skolem_thm ths)
     end;
 
 (**** clausification ****)