1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 13:48:21 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 13:49:44 2010 +0200
     1.3 @@ -145,8 +145,8 @@
     1.4     [maybe_remote_atp thy eN,
     1.5      if forall (is_atp_installed thy) [spassN, eN] then remote_prefix ^ vampireN
     1.6      else maybe_remote_atp thy vampireN,
     1.7 -    remote_prefix ^ sine_eN,
     1.8 -    maybe_remote_smt_solver thy])
     1.9 +    remote_prefix ^ sine_eN (* FIXME: Introduce and document: ,
    1.10 +    maybe_remote_smt_solver thy *)])
    1.11    |> space_implode " "
    1.12  
    1.13  val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param