246 type sdthms = lthms * thm list; |
246 type sdthms = lthms * thm list; |
247 |
247 |
248 fun add_drop_redundant thm thms = |
248 fun add_drop_redundant thm thms = |
249 let |
249 let |
250 val thy = Context.check_thy (Thm.theory_of_thm thm); |
250 val thy = Context.check_thy (Thm.theory_of_thm thm); |
251 val pattern = (fst o Logic.dest_equals o Drule.plain_prop_of) thm; |
251 val args_of = snd o strip_comb o fst o Logic.dest_equals o Drule.plain_prop_of; |
252 fun matches thm' = if (curry (Pattern.matches thy) pattern o |
252 val args = args_of thm; |
253 fst o Logic.dest_equals o Drule.plain_prop_of) thm' |
253 fun matches [] _ = true |
254 then (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); true) |
254 | matches (Var _ :: xs) [] = matches xs [] |
255 else false |
255 | matches (_ :: _) [] = false |
256 in thm :: filter_out matches thms end; |
256 | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys; |
|
257 fun drop thm' = if matches args (args_of thm') |
|
258 then (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); false) |
|
259 else true |
|
260 in thm :: filter drop thms end; |
257 |
261 |
258 fun add_thm thm (sels, dels) = |
262 fun add_thm thm (sels, dels) = |
259 (Susp.value (add_drop_redundant thm (Susp.force sels)), remove eq_thm thm dels); |
263 (Susp.value (add_drop_redundant thm (Susp.force sels)), remove eq_thm thm dels); |
260 |
264 |
261 fun add_lthms lthms (sels, []) = |
265 fun add_lthms lthms (sels, []) = |