# HG changeset patch
# User paulson
# Date 1159803123 -7200
# Node ID 4b48fd429b18c82a5429cfb29f0b38fc823518b3
# Parent  aca7d38283bf988dc4ed4493da7896d71d95a85b
Changing the default for theory_const

diff -r aca7d38283bf -r 4b48fd429b18 src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Mon Oct 02 17:31:14 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Mon Oct 02 17:32:03 2006 +0200
@@ -12,7 +12,7 @@
 struct
 
 val run_relevance_filter = ref true;
-val theory_const = ref false;
+val theory_const = ref true;
 val pass_mark = ref 0.5;
 val convergence = ref 3.2;    (*Higher numbers allow longer inference chains*)
 val max_new = ref 60;         (*Limits how many clauses can be picked up per stage*)