# HG changeset patch
# User paulson
# Date 1192196713 -7200
# Node ID fcf5a999d1c3f9fcf15b54d732dce3212ba12be5
# Parent  60e5516c7b06662ba416149911c82ef7b24103fa
calling the correct interface

diff -r 60e5516c7b06 -r fcf5a999d1c3 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Fri Oct 12 15:21:12 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Fri Oct 12 15:45:13 2007 +0200
@@ -577,7 +577,7 @@
 
 fun cnf_hyps_thms ctxt =
     let val ths = Assumption.prems_of ctxt
-    in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
+    in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom) ths [] end;
 
 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
 datatype mode = Auto | Fol | Hol;