more explicit warning message;

--- a/src/HOL/Tools/metis_tools.ML	Sun Mar 08 17:03:07 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Sun Mar 08 17:05:43 2009 +0100
@@ -608,7 +608,7 @@
 	          val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
               in
                   if null unused then ()
-                  else warning ("Unused theorems: " ^ commas (map #1 unused));
+                  else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
                   case result of
                       (_,ith)::_ => 
                           (Output.debug (fn () => "success: " ^ Display.string_of_thm ith);