--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Nov 18 12:37:30 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Nov 18 18:09:08 2010 +0100
@@ -158,7 +158,7 @@
timeout, it makes sense to put SPASS first. *)
fun default_provers_param_value ctxt =
let val thy = ProofContext.theory_of ctxt in
- [spassN, eN, vampireN, sine_eN (* FIXME: , smtN *)]
+ [spassN, eN, vampireN, sine_eN, smtN]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_local_threads thy (Multithreading.max_threads_value ())
|> space_implode " "