# 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) =