--- a/src/HOL/Tools/ATP/atp_proof.ML Sat Dec 18 12:55:33 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sat Dec 18 13:34:32 2010 +0100
@@ -110,7 +110,7 @@
| string_for_failure prover NoPerl = "Perl" ^ missing_message_tail prover
| string_for_failure prover NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail prover
- | string_for_failure prover NoRealZ3 =
+ | string_for_failure _ NoRealZ3 =
"The environment variable \"Z3_REAL_SOLVER\" must be set to Z3's full path."
| string_for_failure prover MalformedInput =
"The " ^ prover ^ " problem is malformed. Please report this to the \