src/HOL/Tools/res_atp.ML
changeset 20224 9c40a144ee0e
parent 20131 c89ee2f4efd5
child 20246 fdfe7399e057
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jul 27 13:43:00 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jul 27 13:43:01 2006 +0200
     1.3 @@ -576,7 +576,7 @@
     1.4  
     1.5  
     1.6  fun cnf_hyps_thms ctxt = 
     1.7 -    let val ths = ProofContext.prems_of ctxt
     1.8 +    let val ths = Assumption.prems_of ctxt
     1.9      in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
    1.10  
    1.11