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

--- 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 _ =>