# HG changeset patch
# User blanchet
# Date 1309530693 -7200
# Node ID e42ccb132305e353574dbef73ce071789ff823f0
# Parent  030610b1e5a8feef5ef92a9921913ed3e96afbbb
made minimizer informative output accurate

diff -r 030610b1e5a8 -r e42ccb132305 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 01 15:53:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 01 16:31:33 2011 +0200
@@ -173,7 +173,7 @@
            else
              sublinear_minimize (do_test new_timeout) facts ([], result)
          val _ = print silent (fn () => cat_lines
-           ["Minimized to " ^ n_facts used_facts] ^
+           ["Minimized to " ^ n_facts (map fst min_facts)] ^
             (case length (filter (curry (op =) Chained o snd o fst) min_facts) of
                0 => ""
              | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")