fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a

--- 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

--- 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