src/Pure/Tools/find_theorems.ML
changeset 51717 9e7d1c139569
parent 51658 21c10672633b
child 52701 51dfdcd88e84
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -334,7 +334,7 @@
     1.4  
     1.5  fun filter_simp ctxt t (Internal (_, thm)) =
     1.6        let
     1.7 -        val mksimps = Simplifier.mksimps (simpset_of ctxt);
     1.8 +        val mksimps = Simplifier.mksimps ctxt;
     1.9          val extract_simp =
    1.10            (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
    1.11          val ss = is_matching_thm extract_simp ctxt false t thm;