repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 10 01:17:37 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 10 08:23:57 2013 +0200
@@ -1344,7 +1344,7 @@
         (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
         [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
          (mashN, mash |> map fst |> add_and_take)]
-      | (SOME fact_filter, _) => [(fact_filter, mesh)]
+      | _ => [(effective_fact_filter, mesh)]
     end
 
 fun kill_learners ctxt ({overlord, ...} : params) =