# HG changeset patch
# User blanchet
# Date 1272117942 -7200
# Node ID 6adf1068ac0f8b8f24679807e0089471d6df3be8
# Parent  b90fc0d75bca8c35385952e3bfa733dd2b20a431
better error reporting;
in particular, users shouldn't panic if "metis" can prove "False", especially in "neg_clausify"-style proofs

diff -r b90fc0d75bca -r 6adf1068ac0f src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Apr 23 19:36:49 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sat Apr 24 16:05:42 2010 +0200
@@ -352,7 +352,7 @@
         val message =
           #message (prover params (minimize_command name) timeout problem)
           handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line i n []
-               | ERROR msg => "Error: " ^ msg ^ ".\n";
+               | ERROR message => "Error: " ^ message ^ "\n"
         val _ = unregister params message (Thread.self ());
       in () end)
   in () end
diff -r b90fc0d75bca -r 6adf1068ac0f src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Apr 23 19:36:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat Apr 24 16:05:42 2010 +0200
@@ -693,10 +693,11 @@
                 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
                   if common_thm used cls then NONE else SOME name)
             in
-                if not (common_thm used cls) then
-                  warning "Metis: The goal is provable because the context is \
-                          \inconsistent."
-                else if not (null unused) then
+                if not (null cls) andalso not (common_thm used cls) then
+                  warning "Metis: The assumptions are inconsistent."
+                else
+                  ();
+                if not (null unused) then
                   warning ("Metis: Unused theorems: " ^ commas_quote unused
                            ^ ".")
                 else