# HG changeset patch
# User blanchet
# Date 1308559262 -7200
# Node ID b0cf8f9bd1924b584ecb2d081400aae26cd56ea1
# Parent  12ff5c017cf952a58e0a4ecffdfc9fdfc2fbddd2
respect "really_all" argument, which is used by "ATP_Export"

diff -r 12ff5c017cf9 -r b0cf8f9bd192 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- 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