# HG changeset patch
# User blanchet
# Date 1271693685 -7200
# Node ID 43d10a494c913197ddd6ccf1cf1cc6d374adb77c
# Parent  c95fab3f9cc518e5d82cf0453c16c71c7f526e33
added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent

diff -r c95fab3f9cc5 -r 43d10a494c91 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Apr 19 17:18:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Apr 19 18:14:45 2010 +0200
@@ -693,13 +693,19 @@
                 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
                   if common_thm used cls then NONE else SOME name)
             in
-                if null unused then ()
-                else warning ("Metis: unused theorems " ^ commas_quote unused);
+                if not (common_thm used cls) then
+                  warning "Metis: The goal is provable because the context is \
+                          \inconsistent."
+                else if not (null unused) then
+                  warning ("Metis: Unused theorems: " ^ commas_quote unused
+                           ^ ".")
+                else
+                  ();
                 case result of
                     (_,ith)::_ =>
-                        (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith);
+                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
                          [ith])
-                  | _ => (trace_msg (fn () => "Metis: no result");
+                  | _ => (trace_msg (fn () => "Metis: No result");
                           [])
             end
         | Metis.Resolution.Satisfiable _ =>