changeset 32149 | ef59550a55d3 |
parent 32091 | 30e2ffbba718 |
child 32738 | 15bb09ca0378 |
--- a/src/Pure/Tools/find_theorems.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/Pure/Tools/find_theorems.ML Thu Jul 23 18:44:09 2009 +0200 @@ -207,7 +207,7 @@ fun filter_simp ctxt t (_, thm) = let - val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt); + val mksimps = Simplifier.mksimps (simpset_of ctxt); val extract_simp = (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); val ss = is_matching_thm false extract_simp ctxt false t thm;