# HG changeset patch # User blanchet # Date 1298456290 -3600 # Node ID 49d5af6a3d1bbd6a6c2c06d753cec36fdd7e1143 # Parent 81d64ec484278d99c547a281713194d29b06a071# Parent 1b447261865e99804c9835614c1a53447ab18e55 merged diff -r 81d64ec48427 -r 49d5af6a3d1b src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 23 11:16:56 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 23 11:18:10 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