changeset 51717 | 9e7d1c139569 |
parent 51658 | 21c10672633b |
child 52701 | 51dfdcd88e84 |
--- a/src/Pure/Tools/find_theorems.ML Tue Apr 16 17:54:14 2013 +0200 +++ b/src/Pure/Tools/find_theorems.ML Thu Apr 18 17:07:01 2013 +0200 @@ -334,7 +334,7 @@ fun filter_simp ctxt t (Internal (_, thm)) = let - val mksimps = Simplifier.mksimps (simpset_of ctxt); + val mksimps = Simplifier.mksimps 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 extract_simp ctxt false t thm;