src/Pure/Tools/find_theorems.ML
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;