# HG changeset patch
# User wenzelm
# Date 1256824454 -3600
# Node ID a103fa7c19cc3add5673cc9d14b21479f7ffdb18
# Parent  2c77579e05238103d99f15d97c8f87728f7c3ba6
tuned;

diff -r 2c77579e0523 -r a103fa7c19cc src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Oct 29 14:53:53 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Oct 29 14:54:14 2009 +0100
@@ -138,9 +138,9 @@
           val to_use =
             if length ordered_used < length name_thms_pairs then
               filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
-            else
-              name_thms_pairs
-          val (min_thms, n) = if null to_use then ([], 0)
+            else name_thms_pairs
+          val (min_thms, n) =
+            if null to_use then ([], 0)
             else minimal (test_thms (SOME filtered)) to_use
           val min_names = sort_distinct string_ord (map fst min_thms)
           val _ = priority (cat_lines
diff -r 2c77579e0523 -r a103fa7c19cc src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Thu Oct 29 14:53:53 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 29 14:54:14 2009 +0100
@@ -694,10 +694,11 @@
                 and used = map_filter (used_axioms axioms) proof
                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
-                val unused = filter (fn (_, cls) => not (common_thm used cls)) th_cls_pairs
+                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 (map #1 unused));
+                else warning ("Metis: unused theorems " ^ commas_quote unused);
                 case result of
                     (_,ith)::_ =>
                         (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith);