# HG changeset patch
# User blanchet
# Date 1304452009 -7200
# Node ID 390de893659ab8d590359d6ad24cf120ff78fed4
# Parent  45c650e5d0c67c1c5e06d8c8f13b697d518ea408
fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a

diff -r 45c650e5d0c6 -r 390de893659a src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 03 21:46:05 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 03 21:46:49 2011 +0200
@@ -782,7 +782,7 @@
    are omitted. *)
 val is_dangerous_term =
   transform_elim_term
-  #> has_bound_or_var_of_type dangerous_types orf is_exhaustive_finite
+  #> (has_bound_or_var_of_type dangerous_types orf is_exhaustive_finite)
 
 fun is_theorem_bad_for_atps thm =
   let val t = prop_of thm in
diff -r 45c650e5d0c6 -r 390de893659a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 03 21:46:05 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 03 21:46:49 2011 +0200
@@ -441,7 +441,7 @@
                                   ? Integer.min default_max_relevant
                 val fairly_sound = is_type_sys_fairly_sound type_sys
                 val facts =
-                  facts |> fairly_sound
+                  facts |> not fairly_sound
                            ? filter_out (is_dangerous_term o prop_of o snd
                                          o untranslated_fact)
                         |> take num_facts