diff -r 40bf0173fbed -r 96f62b77748f src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 24 00:01:33 2011 +0200
@@ -785,9 +785,9 @@
 (**** Predicates to detect unwanted facts (prolific or likely to cause
       unsoundness) ****)
 
-fun is_theorem_bad_for_atps is_good_prop thm =
+fun is_theorem_bad_for_atps is_appropriate_prop thm =
   let val t = prop_of thm in
-    not (is_good_prop t) orelse is_formula_too_complex t orelse
+    not (is_appropriate_prop t) orelse is_formula_too_complex t orelse
     exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse
     exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
     is_that_fact thm
@@ -815,7 +815,7 @@
      mk_fact_table normalize_simp_prop snd simps)
   end
 
-fun all_facts ctxt reserved really_all is_good_prop add_ths chained_ths =
+fun all_facts ctxt reserved really_all is_appropriate_prop add_ths chained_ths =
   let
     val thy = Proof_Context.theory_of ctxt
     val global_facts = Global_Theory.facts_of thy
@@ -869,8 +869,8 @@
             pair 1
             #> fold (fn th => fn (j, rest) =>
                         (j + 1,
-                         if is_theorem_bad_for_atps is_good_prop th andalso
-                            not (member Thm.eq_thm add_ths th) then
+                         if not (member Thm.eq_thm add_ths th) andalso
+                            is_theorem_bad_for_atps is_appropriate_prop th then
                            rest
                          else
                            (((fn () =>
@@ -903,9 +903,9 @@
 fun external_frees t =
   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
 
-fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_good_prop
-                   is_built_in_const fudge (override as {add, only, ...})
-                   chained_ths hyp_ts concl_t =
+fun relevant_facts ctxt (threshold0, threshold1) max_relevant
+        is_appropriate_prop is_built_in_const fudge
+        (override as {add, only, ...}) chained_ths hyp_ts concl_t =
   let
     val thy = Proof_Context.theory_of ctxt
     val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
@@ -921,7 +921,7 @@
          maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
                o fact_from_ref ctxt reserved chained_ths) add
        else
-         all_facts ctxt reserved false is_good_prop add_ths chained_ths)
+         all_facts ctxt reserved false is_appropriate_prop add_ths chained_ths)
       |> Config.get ctxt instantiate_inducts
          ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
       |> rearrange_facts ctxt only