--- 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);
--- 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