# HG changeset patch
# User blanchet
# Date 1392293777 -3600
# Node ID 0b070d098d1a4474e829157391282f5ce6803dea
# Parent  29ec8680e61f7f0b6bcb4b59be5530668af49c7d
repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial

diff -r 29ec8680e61f -r 0b070d098d1a src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 13:16:17 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -118,17 +118,16 @@
 
 val is_atp = member (op =) o supported_atps
 
-fun remotify_atp_if_supported_and_not_already_remote thy name =
-  if String.isPrefix remote_prefix name then
-    SOME name
+fun remotify_atp_if_not_installed thy name =
+  if is_atp thy name then
+    if String.isPrefix remote_prefix name orelse is_atp_installed thy name then
+      SOME name
+    else
+      let val remote_name = remote_prefix ^ name in
+        if is_atp thy remote_name then SOME remote_name else NONE
+      end
   else
-    let val remote_name = remote_prefix ^ name in
-      if is_atp thy remote_name then SOME remote_name else NONE
-    end
-
-fun remotify_atp_if_not_installed thy name =
-  if is_atp thy name andalso is_atp_installed thy name then SOME name
-  else remotify_atp_if_supported_and_not_already_remote thy name
+    SOME name
 
 type params =
   {debug : bool,