src/Pure/Tools/find_theorems.ML
changeset 33039 5018f6a76b3f
parent 33036 c61fe520602b
parent 33038 8f9594c31de4
child 33095 bbd52d2f8696
--- a/src/Pure/Tools/find_theorems.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -248,7 +248,7 @@
 
     fun check (t, NONE) = check (t, SOME (get_thm_names t))
       | check ((_, thm), c as SOME thm_consts) =
-         (if pat_consts subset_string thm_consts andalso
+         (if subset (op =) (pat_consts, thm_consts) andalso
             Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
           then SOME (0, 0) else NONE, c);
   in check end;