author | paulson |
Fri, 12 Oct 2007 15:45:13 +0200 | |
changeset 25006 | fcf5a999d1c3 |
parent 25005 | 60e5516c7b06 |
child 25007 | cd497f6fe8d1 |
--- 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;