--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 14 12:54:26 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 14 13:20:59 2012 +0200
@@ -87,7 +87,7 @@
fun print_used_facts used_facts =
tag_list 1 facts
|> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
- |> filter_used_facts used_facts
+ |> filter_used_facts false used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas
|> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^