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