equal
deleted
inserted
replaced
246 let |
246 let |
247 val pat_consts = get_names pat; |
247 val pat_consts = get_names pat; |
248 |
248 |
249 fun check (t, NONE) = check (t, SOME (get_thm_names t)) |
249 fun check (t, NONE) = check (t, SOME (get_thm_names t)) |
250 | check ((_, thm), c as SOME thm_consts) = |
250 | check ((_, thm), c as SOME thm_consts) = |
251 (if pat_consts subset_string thm_consts andalso |
251 (if subset (op =) (pat_consts, thm_consts) andalso |
252 Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm) |
252 Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm) |
253 then SOME (0, 0) else NONE, c); |
253 then SOME (0, 0) else NONE, c); |
254 in check end; |
254 in check end; |
255 |
255 |
256 |
256 |