src/HOL/Tools/res_atp.ML
changeset 19617 7cb4b67d4b97
parent 19490 bf7f8347174a
child 19641 f1de44e61ec1
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu May 11 19:15:16 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu May 11 19:19:31 2006 +0200
     1.3 @@ -269,9 +269,7 @@
     1.4  
     1.5  fun cnf_hyps_thms ctxt = 
     1.6      let val ths = ProofContext.prems_of ctxt
     1.7 -    in
     1.8 -	ResClause.union_all (map ResAxioms.skolem_thm ths)
     1.9 -    end;
    1.10 +    in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
    1.11  
    1.12  
    1.13  (**** write to files ****)