# HG changeset patch
# User wenzelm
# Date 1236528343 -3600
# Node ID 4ec39edb88b131a26cd66b812d8ff0ecaf560a11
# Parent  8ea7a197e2e6415f13dc95343ed1266bee7139a1
more explicit warning message;

diff -r 8ea7a197e2e6 -r 4ec39edb88b1 src/HOL/Tools/metis_tools.ML
--- 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);