# HG changeset patch
# User blanchet
# Date 1381386237 -7200
# Node ID 8ab8794410cd268b7674c3e40981aace67599127
# Parent  d80743f28fec7c8cb5c74be1f61e2aac83e2fd44
repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions

diff -r d80743f28fec -r 8ab8794410cd src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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) =