changeset 43477 | b0cf8f9bd192 |
parent 43421 | 926bfe067a32 |
child 43492 | 43326cadc31a |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jun 20 10:41:02 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jun 20 10:41:02 2011 +0200 @@ -867,7 +867,8 @@ pair 1 #> fold (fn th => fn (j, (multis, unis)) => (j + 1, - if not (member Thm.eq_thm_prop add_ths th) andalso + if not really_all andalso + not (member Thm.eq_thm_prop add_ths th) andalso is_theorem_bad_for_atps th then (multis, unis) else