remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
authorblanchet
Thu, 22 Apr 2010 16:30:54 +0200
changeset 36290 c29283184c7a
parent 36289 f75b6a3e1450
child 36291 b4c2043cc96c
remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
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"