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