# HG changeset patch
# User blanchet
# Date 1334663671 -7200
# Node ID da72e05849ef0a9890ed4da0a85931a741462d68
# Parent  e33d957ae2bf574ec9602c8c7102589f8f2e5829
more helpful error message

diff -r e33d957ae2bf -r da72e05849ef src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Apr 17 13:54:31 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Apr 17 13:54:31 2012 +0200
@@ -109,7 +109,7 @@
     "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
     " "
 
-fun string_for_failure Unprovable = "The problem is unprovable."
+fun string_for_failure Unprovable = "The generated problem is unprovable."
   | string_for_failure GaveUp = "The prover gave up."
   | string_for_failure ProofMissing =
     "The prover claims the conjecture is a theorem but did not provide a proof."
@@ -128,7 +128,7 @@
   | string_for_failure CantConnect = "Cannot connect to remote server."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure Inappropriate =
-    "The problem lies outside the prover's scope."
+    "The generated problem lies outside the prover's scope."
   | string_for_failure OutOfResources = "The prover ran out of resources."
   | string_for_failure NoPerl = "Perl" ^ missing_message_tail
   | string_for_failure NoLibwwwPerl =
diff -r e33d957ae2bf -r da72e05849ef src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Apr 17 13:54:31 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Apr 17 13:54:31 2012 +0200
@@ -639,6 +639,7 @@
   remote_atp waldmeisterN "Waldmeister" ["710"]
       [("#START OF PROOF", "Proved Goals:")]
       [(OutOfResources, "Too many function symbols"),
+       (Inappropriate, "****  Unexpected end of file."),
        (Crashed, "Unrecoverable Segmentation Fault")]
       Hypothesis Hypothesis
       (K ((50, CNF_UEQ, "mono_tags??", combsN, false), "") (* FUDGE *))