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