# HG changeset patch
# User blanchet
# Date 1283966452 -7200
# Node ID eec61233dbad9d18fb0a681ed6b67cee887c855b
# Parent  022f16801e4ecec37614dbd164d87a3b07d45f63
improve SInE-E failure message

diff -r 022f16801e4e -r eec61233dbad src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 08 16:01:06 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 08 19:20:52 2010 +0200
@@ -285,7 +285,7 @@
 val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
 val remote_vampire = remotify_prover vampire "Vampire" ["9.0", "1.0", "0.6"]
 val remote_sine_e =
-  remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
+  remote_prover "sine_e" "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
                 800 (* FUDGE *) true
 val remote_snark =
   remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []