--- 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)") ^ ".")