--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Sep 03 15:47:39 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Sep 03 17:55:31 2009 +0200
@@ -83,7 +83,7 @@
("# Cannot determine problem status within resource limit", Timeout),
("Error", Error)]
-fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
+fun produce_answer (success, message, _, result_string, thm_name_vec, filtered) =
if success then
(Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
else