# HG changeset patch
# User blanchet
# Date 1362660294 -3600
# Node ID 4b5a5e26161d757f84f438e6236f4c35c14e59b7
# Parent  abdcf1a7cabf2eeda954e282fc6acc268a098d78
better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)

diff -r abdcf1a7cabf -r 4b5a5e26161d src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Mar 06 10:44:43 2013 -0800
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Mar 07 13:44:54 2013 +0100
@@ -113,14 +113,13 @@
     "The prover claims the conjecture is a theorem but provided an incomplete \
     \(or unparsable) proof."
   | string_for_failure (UnsoundProof (false, ss)) =
-    "The prover found a type-unsound proof " ^ involving ss ^
+    "The prover found an unsound proof " ^ involving ss ^
     "(or, less likely, your axioms are inconsistent). Specify a sound type \
     \encoding or omit the \"type_enc\" option."
   | 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). Please report this to the Isabelle \
-    \developers."
+    "The prover found an unsound proof " ^ involving ss ^
+    "(or, less likely, 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 =