src/Pure/Tools/find_theorems.ML
changeset 33038 8f9594c31de4
parent 33037 b22e44496dc2
child 33039 5018f6a76b3f
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Oct 20 16:13:01 2009 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Oct 21 08:14:38 2009 +0200
     1.3 @@ -227,7 +227,7 @@
     1.4  
     1.5      fun check (t, NONE) = check (t, SOME (get_thm_names t))
     1.6        | check ((_, thm), c as SOME thm_consts) =
     1.7 -         (if gen_subset (op =) (pat_consts, thm_consts) andalso
     1.8 +         (if subset (op =) (pat_consts, thm_consts) andalso
     1.9              Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
    1.10            then SOME (0, 0) else NONE, c);
    1.11    in check end;