--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Jun 06 20:36:34 2011 +0200
@@ -185,7 +185,8 @@
string_of_int (10 + msecs div 1000) ^ "\")."))
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message)))
- handle ERROR msg => (NONE, (K Failed_to_Play, fn _ => "Error: " ^ msg))
+ handle ERROR msg =>
+ (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg))
end
fun run_minimize (params as {provers, ...}) i refs state =