diff -r 550f265864e3 -r 98fb341d32e3 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 07 11:57:42 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 07 14:05:32 2013 +0100
@@ -634,7 +634,7 @@
         ({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
           best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
         (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
-                    uncurried_aliases, max_facts, max_mono_iters,
+                    uncurried_aliases, fact_filter, max_facts, max_mono_iters,
                     max_new_mono_instances, isar_proofs, isar_shrink,
                     slice, timeout, preplay_timeout, ...})
         minimize_command
@@ -720,7 +720,9 @@
                               best_uncurried_aliases),
                       extra))) =
           let
-            val facts = get_facts_for_filter best_fact_filter factss
+            val effective_fact_filter =
+              fact_filter |> the_default best_fact_filter
+            val facts = get_facts_for_filter effective_fact_filter factss
             val num_facts =
               length facts |> is_none max_facts ? Integer.min best_max_facts
             val soundness = if strict then Strict else Non_Strict
@@ -988,7 +990,8 @@
     val ctxt = Proof.context_of state |> repair_context
     val state = state |> Proof.map_context (K ctxt)
     val max_slices = if slice then Config.get ctxt smt_max_slices else 1
-    fun do_slice timeout slice outcome0 time_so_far weighted_factss =
+    fun do_slice timeout slice outcome0 time_so_far
+                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
       let
         val timer = Timer.startRealTimer ()
         val state =
@@ -1007,7 +1010,6 @@
             end
           else
             timeout
-        val weighted_facts = hd weighted_factss
         val num_facts = length weighted_facts
         val _ =
           if debug then
@@ -1056,21 +1058,27 @@
             val new_num_facts =
               Real.ceil (Config.get ctxt smt_slice_fact_frac
                          * Real.fromInt num_facts)
+            val weighted_factss as (new_fact_filter, _) :: _ =
+              weighted_factss
+              |> rotate_one
+              |> app_hd (apsnd (take new_num_facts))
+            val show_filter = fact_filter <> new_fact_filter
+            fun num_of_facts fact_filter num_facts =
+              string_of_int num_facts ^
+              (if show_filter then " " ^ quote fact_filter else "") ^
+              " fact" ^ plural_s num_facts
             val _ =
               if verbose andalso is_some outcome then
-                quote name ^ " invoked with " ^ string_of_int num_facts ^
-                " fact" ^ plural_s num_facts ^ ": " ^
+                quote name ^ " invoked with " ^
+                num_of_facts fact_filter num_facts ^ ": " ^
                 string_for_failure (failure_from_smt_failure (the outcome)) ^
-                " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^
-                plural_s new_num_facts ^ "..."
+                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
+                "..."
                 |> Output.urgent_message
               else
                 ()
           in
-            weighted_factss
-            |> rotate_one
-            |> app_hd (take new_num_facts)
-            |> do_slice timeout (slice + 1) outcome0 time_so_far
+            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
           end
         else
           {outcome = if is_none outcome then NONE else the outcome0,
@@ -1089,7 +1097,7 @@
         facts ~~ (0 upto num_facts - 1)
         |> map (weight_smt_fact ctxt num_facts)
       end
-    val weighted_factss = factss |> map (snd #> weight_facts)
+    val weighted_factss = factss |> map (apsnd weight_facts)
     val {outcome, used_facts = used_pairs, used_from, run_time} =
       smt_filter_loop name params state goal subgoal weighted_factss
     val used_facts = used_pairs |> map fst