1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Feb 08 08:58:24 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Feb 08 16:10:06 2011 +0100
     1.3 @@ -281,8 +281,8 @@
     1.4  fun proof_banner auto =
     1.5    if auto then "Auto Sledgehammer found a proof" else "Try this command"
     1.6  
     1.7 -val smt_triggers = Unsynchronized.ref false
     1.8 -val smt_weights = Unsynchronized.ref false
     1.9 +val smt_triggers = Unsynchronized.ref true
    1.10 +val smt_weights = Unsynchronized.ref true
    1.11  val smt_weight_min_facts = Unsynchronized.ref 20
    1.12  
    1.13  (* FUDGE *)