# HG changeset patch
# User wenzelm
# Date 1565617481 -7200
# Node ID dc749e0dc6b290bd52a1e98cdf75c6d7a63b9ab9
# Parent  06425eaa9cd7d67c521e08c8934662ddc6ad4c70
tuned;

diff -r 06425eaa9cd7 -r dc749e0dc6b2 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Aug 12 15:43:05 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Aug 12 15:44:41 2019 +0200
@@ -208,15 +208,12 @@
             val used = map_filter (used_axioms axioms) proof
             val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
             val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
-            val (used_th_cls_pairs, unused_th_cls_pairs) =
-              List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
-            val unused_ths = maps (snd o snd) unused_th_cls_pairs
-            val unused_names = map fst unused_th_cls_pairs
 
-            val _ = unused := unused_ths;
+            val unused_th_cls_pairs = filter_out (have_common_thm ctxt used o #2 o #2) th_cls_pairs
+            val _ = unused := maps (#2 o #2) unused_th_cls_pairs;
             val _ =
-              if not (null unused_names) then
-                verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused_names)
+              if not (null unused_th_cls_pairs) then
+                verbose_warning ctxt ("Unused theorems: " ^ commas_quote (map #1 unused_th_cls_pairs))
               else ();
             val _ =
               if not (null cls) andalso not (have_common_thm ctxt used cls) then