# HG changeset patch
# User blanchet
# Date 1308499969 -7200
# Node ID 5ca37e76413965f759331327c602b71e6679eb87
# Parent  71b7a535cf9619d0a1d85c311e255d6973f5ca33
more forceful message

diff -r 71b7a535cf96 -r 5ca37e764139 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Jun 19 00:03:44 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun Jun 19 18:12:49 2011 +0200
@@ -129,8 +129,8 @@
   | string_for_failure (UnsoundProof (true, ss)) =
     "The prover found a type-unsound proof " ^ involving ss ^
     "even though a supposedly type-sound encoding was used (or, less likely, \
-    \your axioms are inconsistent). You might want to report this to the \
-    \Isabelle developers."
+    \your axioms are inconsistent). Please report this to the Isabelle \
+    \developers."
   | string_for_failure CantConnect = "Cannot connect to remote server."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure Inappropriate =