# HG changeset patch
# User blanchet
# Date 1297177806 -3600
# Node ID bb366da22483e3b38434a9a057b7d2c36138b034
# Parent  9575694d2da50e3d51150e274fcbbbfad6b742ef
enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite

diff -r 9575694d2da5 -r bb366da22483 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Feb 08 08:58:24 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Feb 08 16:10:06 2011 +0100
@@ -281,8 +281,8 @@
 fun proof_banner auto =
   if auto then "Auto Sledgehammer found a proof" else "Try this command"
 
-val smt_triggers = Unsynchronized.ref false
-val smt_weights = Unsynchronized.ref false
+val smt_triggers = Unsynchronized.ref true
+val smt_weights = Unsynchronized.ref true
 val smt_weight_min_facts = Unsynchronized.ref 20
 
 (* FUDGE *)