remove hack that is no longer necessary now that "ATP_Wrapper" properly detects which ATPs are installed
--- 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"