# HG changeset patch
# User wenzelm
# Date 1304454499 -7200
# Node ID d34154b085797bb86f841eb6c1c0629143f215e4
# Parent  390de893659ab8d590359d6ad24cf120ff78fed4# Parent  04dfffda56712ade590891db12b456c187c824b6
merged

diff -r 04dfffda5671 -r d34154b08579 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 03 22:27:32 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 03 22:28:19 2011 +0200
@@ -134,8 +134,8 @@
   | level_of_type_sys (Preds (_, level)) = level
   | level_of_type_sys (Tags (_, level)) = level
 
-val is_type_level_virtually_sound =
-  member (op =) [All_Types, Nonmonotonic_Types]
+fun is_type_level_virtually_sound s =
+  s = All_Types orelse s = Nonmonotonic_Types
 val is_type_sys_virtually_sound =
   is_type_level_virtually_sound o level_of_type_sys
 
diff -r 04dfffda5671 -r d34154b08579 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 03 22:27:32 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 03 22:28:19 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 04dfffda5671 -r d34154b08579 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 03 22:27:32 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 03 22:28:19 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