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