minor bug fixes
authorpaulson
Mon Aug 28 18:18:31 2006 +0200 (2006-08-28 ago)
changeset 20423593053389701
parent 20422 35a6a4c863f1
child 20424 d5b4b55ad277
minor bug fixes
src/HOL/Tools/ATP/reduce_axiomsN.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Mon Aug 28 18:16:08 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Mon Aug 28 18:18:31 2006 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  val pass_mark = ref 0.6;
     1.6  val convergence = ref 2.4;   (*Higher numbers allow longer inference chains*)
     1.7 -val follow_defs = ref true;  (*Follow definitions. Makes problems bigger.*)
     1.8 +val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
     1.9  
    1.10  fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
    1.11  
     2.1 --- a/src/HOL/Tools/res_atp.ML	Mon Aug 28 18:16:08 2006 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Aug 28 18:18:31 2006 +0200
     2.3 @@ -735,7 +735,7 @@
     2.4  	      let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, 
     2.5  	                                   skolemize_tac] n th)
     2.6  		  val negs = Option.valOf (metahyps_thms n st)
     2.7 -		  val negs_clauses = ResAxioms.assume_abstract (make_clauses negs)
     2.8 +		  val negs_clauses = make_clauses (ResAxioms.assume_abstract negs)
     2.9  	      in
    2.10  		  negs_clauses :: get_neg_subgoals (n-1)
    2.11  	      end