src/HOL/Tools/res_atp.ML
changeset 20423 593053389701
parent 20419 df257a9cf0e9
child 20444 6c5e38a73db0
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Aug 28 18:16:08 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Aug 28 18:18:31 2006 +0200
     1.3 @@ -735,7 +735,7 @@
     1.4  	      let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, 
     1.5  	                                   skolemize_tac] n th)
     1.6  		  val negs = Option.valOf (metahyps_thms n st)
     1.7 -		  val negs_clauses = ResAxioms.assume_abstract (make_clauses negs)
     1.8 +		  val negs_clauses = make_clauses (ResAxioms.assume_abstract negs)
     1.9  	      in
    1.10  		  negs_clauses :: get_neg_subgoals (n-1)
    1.11  	      end