# HG changeset patch
# User blanchet
# Date 1287748184 -7200
# Node ID 80d4ea0e536a2ef7dba7e962c274bbe0a731c67e
# Parent  1e4c7185f3f99daea69c13c29408f586f0b58754
took out "smt"/"remote_smt" from default ATPs until they are properly implemented

diff -r 1e4c7185f3f9 -r 80d4ea0e536a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 13:48:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 13:49:44 2010 +0200
@@ -145,8 +145,8 @@
    [maybe_remote_atp thy eN,
     if forall (is_atp_installed thy) [spassN, eN] then remote_prefix ^ vampireN
     else maybe_remote_atp thy vampireN,
-    remote_prefix ^ sine_eN,
-    maybe_remote_smt_solver thy])
+    remote_prefix ^ sine_eN (* FIXME: Introduce and document: ,
+    maybe_remote_smt_solver thy *)])
   |> space_implode " "
 
 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param