# HG changeset patch
# User paulson
# Date 1156781911 -7200
# Node ID 593053389701f0f31851f36d17d16fce1e9bafdf
# Parent  35a6a4c863f1067510d66c06590bc77431516eb1
minor bug fixes

diff -r 35a6a4c863f1 -r 593053389701 src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Mon Aug 28 18:16:08 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Mon Aug 28 18:18:31 2006 +0200
@@ -7,7 +7,7 @@
 
 val pass_mark = ref 0.6;
 val convergence = ref 2.4;   (*Higher numbers allow longer inference chains*)
-val follow_defs = ref true;  (*Follow definitions. Makes problems bigger.*)
+val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
 
 fun log_weight2 (x:real) = 1.0 + 2.0/Math.ln (x+1.0);
 
diff -r 35a6a4c863f1 -r 593053389701 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Aug 28 18:16:08 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon Aug 28 18:18:31 2006 +0200
@@ -735,7 +735,7 @@
 	      let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, 
 	                                   skolemize_tac] n th)
 		  val negs = Option.valOf (metahyps_thms n st)
-		  val negs_clauses = ResAxioms.assume_abstract (make_clauses negs)
+		  val negs_clauses = make_clauses (ResAxioms.assume_abstract negs)
 	      in
 		  negs_clauses :: get_neg_subgoals (n-1)
 	      end