equal
deleted
inserted
replaced
225 let |
225 let |
226 val pat_consts = get_names pat; |
226 val pat_consts = get_names pat; |
227 |
227 |
228 fun check (t, NONE) = check (t, SOME (get_thm_names t)) |
228 fun check (t, NONE) = check (t, SOME (get_thm_names t)) |
229 | check ((_, thm), c as SOME thm_consts) = |
229 | check ((_, thm), c as SOME thm_consts) = |
230 (if pat_consts subset_string thm_consts andalso |
230 (if gen_subset (op =) (pat_consts, thm_consts) andalso |
231 Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm) |
231 Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm) |
232 then SOME (0, 0) else NONE, c); |
232 then SOME (0, 0) else NONE, c); |
233 in check end; |
233 in check end; |
234 |
234 |
235 |
235 |