make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jun 23 18:43:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jun 24 10:38:01 2010 +0200
@@ -679,8 +679,7 @@
       (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
       fun set_mode FO = FO
         | set_mode HO =
-          if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
-          else HO
+          if forall (is_quasi_fol_theorem thy) (cls @ ths) then FO else HO
         | set_mode FT = FT
       val mode = set_mode mode0
       (*transform isabelle clause to metis clause *)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Jun 23 18:43:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Jun 24 10:38:01 2010 +0200
@@ -21,7 +21,7 @@
   val tvar_classes_of_terms : term list -> string list
   val tfree_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
-  val is_quasi_fol_term : theory -> term -> bool
+  val is_quasi_fol_theorem : theory -> thm -> bool
   val relevant_facts :
     bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
     -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
@@ -352,7 +352,11 @@
 fun relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant relevance_override
                      thy (axioms : cnf_thm list) goals =
-  if relevance_threshold > 0.0 then
+  if relevance_threshold > 1.0 then
+    []
+  else if relevance_threshold < 0.0 then
+    axioms
+  else
     let
       val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
                            Symtab.empty
@@ -370,8 +374,6 @@
       trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
       relevant
     end
-  else
-    axioms;
 
 (***************************************************************)
 (* Retrieving and filtering lemmas                             *)
@@ -513,13 +515,8 @@
 (* ATP invocation methods setup                                *)
 (***************************************************************)
 
-fun is_quasi_fol_term thy =
-  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 []
-
-(*Ensures that no higher-order theorems "leak out"*)
-fun restrict_to_logic thy true cls =
-    filter (is_quasi_fol_term thy o prop_of o fst) cls
-  | restrict_to_logic _ false cls = cls
+fun is_quasi_fol_theorem thy =
+  Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
 
 (**** Predicates to detect unwanted clauses (prolific or likely to cause
       unsoundness) ****)
@@ -569,43 +566,35 @@
     (has_typed_var dangerous_types t orelse
      forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
 
-fun remove_dangerous_clauses full_types add_thms =
-  filter_out (fn (cnf_th, (_, orig_th)) =>
-                 not (member Thm.eq_thm add_thms orig_th) andalso
-                 is_dangerous_term full_types (prop_of cnf_th))
-
 fun is_fol_goal thy = forall (Meson.is_fol_term thy) o map prop_of
 
 fun relevant_facts full_types respect_no_atp relevance_threshold
                    relevance_convergence defs_relevant max_new theory_relevant
                    (relevance_override as {add, del, only})
                    (ctxt, (chained_ths, _)) goal_cls =
-  if (only andalso null add) orelse relevance_threshold > 1.0 then
-    []
-  else
-    let
-      val thy = ProofContext.theory_of ctxt
-      val has_override = not (null add) orelse not (null del)
-      val is_FO = is_fol_goal thy goal_cls
-      val axioms =
-        checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
-            (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
-             else all_name_thms_pairs respect_no_atp ctxt chained_ths)
-        |> cnf_rules_pairs thy
-        |> not has_override ? make_unique
-        |> not only ? restrict_to_logic thy is_FO
-        |> (if only then
-              I
-            else
-              remove_dangerous_clauses full_types
-                                       (maps (ProofContext.get_fact ctxt) add))
-    in
-      relevance_filter ctxt relevance_threshold relevance_convergence
-                       defs_relevant max_new theory_relevant relevance_override
-                       thy axioms (map prop_of goal_cls)
-      |> has_override ? make_unique
-      |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
-    end
+  let
+    val thy = ProofContext.theory_of ctxt
+    val add_thms = maps (ProofContext.get_fact ctxt) add
+    val has_override = not (null add) orelse not (null del)
+    val is_FO = is_fol_goal thy goal_cls
+    val axioms =
+      checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
+          (map (name_thms_pair_from_ref ctxt chained_ths) add @
+           (if only then []
+            else all_name_thms_pairs respect_no_atp ctxt chained_ths))
+      |> cnf_rules_pairs thy
+      |> not has_override ? make_unique
+      |> filter (fn (cnf_thm, (_, orig_thm)) =>
+                    member Thm.eq_thm add_thms orig_thm orelse
+                    ((not is_FO orelse is_quasi_fol_theorem thy cnf_thm) andalso
+                     not (is_dangerous_term full_types (prop_of cnf_thm))))
+  in
+    relevance_filter ctxt relevance_threshold relevance_convergence
+                     defs_relevant max_new theory_relevant relevance_override
+                     thy axioms (map prop_of goal_cls)
+    |> has_override ? make_unique
+    |> sort (prod_ord string_ord int_ord o pairself (fst o snd))
+  end
 
 (** Helper clauses **)