src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML

 end;
 
 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
 struct
 
+open Sledgehammer_Util
+
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
 val respect_no_atp = true
 

   let
     val ths = ProofContext.get_fact ctxt xref
     val name = Facts.string_of_ref xref
                |> forall (member Thm.eq_thm chained_ths) ths
                   ? prefix chained_prefix
-  in (name, ths |> map Clausifier.transform_elim_theorem) end
+  in (name, ths) end
 
 
 (***************************************************************)
 (* Relevance Filtering                                         *)
 (***************************************************************)

   apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
 
 val exists_sledgehammer_const =
   exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
 
-fun is_strange_thm th =
+fun is_strange_theorem th =
   case head_of (concl_of th) of
       Const (a, _) => (a <> @{const_name Trueprop} andalso
                        a <> @{const_name "=="})
     | _ => false
 

 (* Facts containing variables of type "unit" or "bool" or of the form
    "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
    are omitted. *)
 fun is_dangerous_term full_types t =
   not full_types andalso
-  (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t)
+  ((has_bound_or_var_of_type dangerous_types t andalso
+    has_bound_or_var_of_type dangerous_types (transform_elim_term t))
+   orelse is_exhaustive_finite t)
 
 fun is_theorem_bad_for_atps full_types thm =
   let val t = prop_of thm in
     is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
     is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
-    is_strange_thm thm
+    is_strange_theorem thm
   end
 
 fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);

                 NONE => false
               | SOME ths1 => Thm.eq_thms (ths0, ths1))
             val name1 = Facts.extern facts name;
             val name2 = Name_Space.extern full_space name;
             val ths =
-              ths0 |> map Clausifier.transform_elim_theorem
-                   |> filter ((not o is_theorem_bad_for_atps full_types) orf
+              ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf
                               member Thm.eq_thm add_thms)
             val name' =
               case find_first check_thms [name1, name2, name] of
                 SOME name' => name'
               | NONE =>

                                "`" ^ Print_Mode.setmp [Print_Mode.input]
                                          (Syntax.string_of_term ctxt)
                                          (prop_of th) ^ "`")
                     |> space_implode " "
           in
-            cons (name' |> forall (member Thm.eq_thm chained_ths) ths
+            cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
                            ? prefix chained_prefix, ths)
           end)
   in
     valid_facts local_facts (unnamed_locals @ named_locals) @
     valid_facts global_facts (Facts.dest_static [] global_facts)