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;