# HG changeset patch
# User blanchet
# Date 1271946654 -7200
# Node ID c29283184c7a83959bf03c4372de3f7c0c455cc1
# Parent  f75b6a3e14505310713059e6f9d7a75e723a1f00
remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed

diff -r f75b6a3e1450 -r c29283184c7a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Apr 22 16:30:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Apr 22 16:30:54 2010 +0200
@@ -102,19 +102,11 @@
   val extend = I
   fun merge p : T = AList.merge (op =) (K true) p)
 
-(* Don't even try to start ATPs that are not installed.
-   Hack: Should not rely on naming convention. *)
-val filter_atps =
-  space_explode " "
-  #> filter (fn s => String.isPrefix "remote_" s orelse
-                     getenv (String.map Char.toUpper s ^ "_HOME") <> "")
-  #> space_implode " "
-
 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
 fun default_raw_params thy =
   Data.get thy
   |> fold (AList.default (op =))
-          [("atps", [filter_atps (!atps)]),
+          [("atps", [!atps]),
            ("full_types", [if !full_types then "true" else "false"]),
            ("timeout", let val timeout = !timeout in
                          [if timeout <= 0 then "none"