# HG changeset patch
# User blanchet
# Date 1298456268 -3600
# Node ID 1b447261865e99804c9835614c1a53447ab18e55
# Parent  c118ae98dfbf8132b1ec0ee0873177de867afc77
remove confusing message

diff -r c118ae98dfbf -r 1b447261865e src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 23 10:48:57 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 23 11:17:48 2011 +0100
@@ -178,12 +178,6 @@
        (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
               \option (e.g., \"timeout = " ^
               string_of_int (10 + msecs div 1000) ^ "\").")
-     | {outcome = SOME (UnknownError _), ...} =>
-       (* Failure sometimes mean timeout, unfortunately. *)
-       (NONE, "Failure: No proof was found with the current time limit. You \
-              \can increase the time limit using the \"timeout\" \
-              \option (e.g., \"timeout = " ^
-              string_of_int (10 + msecs div 1000) ^ "\").")
      | {message, ...} => (NONE, "Prover error: " ^ message))
     handle ERROR msg => (NONE, "Error: " ^ msg)
   end