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